Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Number of open issues is less than 100 #470

Closed
brianhuffman opened this issue Oct 5, 2017 · 14 comments
Closed

Number of open issues is less than 100 #470

brianhuffman opened this issue Oct 5, 2017 · 14 comments

Comments

@brianhuffman
Copy link
Contributor

For much of Cryptol's history we've had at least a hundred open tickets on the github issue tracker. Lately we've dipped below 100, which probably means that we're getting a little behind on filing new ones.

We should close this ticket once the number is back up where it should be; of course it might be necessary to open the ticket again if the numbers dip again in the future.

@TomMD
Copy link
Contributor

TomMD commented Oct 6, 2017

We still need three more issues at time or writing. I can revert the oldest 3 bug fixes that revert cleanly and re-open those tickets. Thoughts?

@yav
Copy link
Member

yav commented Oct 6, 2017

Hm, I am sensing a problem here. Say we introduced 3 more issues. Then we would be at a 100 issues, which means that we could close this ticket, but then we'd have to open it straight away...

@elliottt
Copy link
Contributor

elliottt commented Oct 9, 2017

Clearly someone will need to take on the full time opening/closing responsibility. Nominations for the position?

@weaversa
Copy link
Collaborator

weaversa commented Nov 6, 2017

Currently in QuasiSpace here.

@brianhuffman
Copy link
Contributor Author

We're currently at 101, so I'm closing this ticket for now.

@yav
Copy link
Member

yav commented Jul 24, 2018

Uhm, things seem to be getting worse.

@brianhuffman
Copy link
Contributor Author

It seems like we're doing a pretty good job of filing new tickets lately: In the past month (June 24 to July 24) we have seen one pull request and 22 new tickets filed (#517 to #539), up from only 8 the previous month. But apparently we need to work even harder!

@weaversa
Copy link
Collaborator

weaversa commented Nov 2, 2018

79 is pretty good!

@brianhuffman
Copy link
Contributor Author

With #599, we now have more than 100 issues again.

@robdockins
Copy link
Contributor

🤷

@robdockins robdockins reopened this Jun 24, 2019
@brianhuffman
Copy link
Contributor Author

brianhuffman commented Jun 24, 2019

I just opened 4 new tickets! See #616, #617, #618, and #619. This brings us back up over 100.

@brianhuffman
Copy link
Contributor Author

Once again we're comfortably over the 100 mark.

@weaversa
Copy link
Collaborator

weaversa commented Jul 3, 2020

Just dipped under.

@weaversa weaversa reopened this Jul 3, 2020
@WeeknightMVP
Copy link

This issue can be closed again for now. Perhaps you could use the GitHub API to dynamically update the issue status? Sounds like a great use of bandwidth! (For this, the guide suggests a webhook, as aggressive polling is frowned upon.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

7 participants