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

time: refactor, add notion of days a PR has been sitting #37

Merged
merged 4 commits into from Jan 11, 2019

Conversation

Projects
None yet
7 participants
@jeffkaufman
Copy link
Owner

jeffkaufman commented Jan 8, 2019

  • refactor time handling
  • add caching of pr_json from github
  • add a notion of the number of days a PR has been sitting

This is #29 with all the functionality changes removed.

jeffkaufman added some commits Jan 6, 2019

approval-threshold: allow changes to go in with majority approval if …
…it's been sitting for a day with no rejections

At some point we may want to allow things to go in over someone's rejection: this is not that.  Any player can still reject any PR and stop it.  But if a PR has no rejections, has been approved by a majority of players, and not been updated in the last day, allow it to go in.

Also refactor time-related functions.

@pavellishin pavellishin requested a review from jmitchell Jan 8, 2019

@vesche

vesche approved these changes Jan 9, 2019

@pavellishin

This comment has been minimized.

Copy link
Collaborator

pavellishin commented Jan 9, 2019

Oh no, conflicts!

@jeffkaufman

This comment has been minimized.

Copy link
Owner Author

jeffkaufman commented Jan 9, 2019

Oh no, conflicts!

addressed in 0edbac9; needs re-review :(

@TheJhyde
Copy link
Contributor

TheJhyde left a comment

Ok fine. But only because my attempt at trickery using the git time stamps (#32) turned out to be nonviable. You'd have to edit the merge timestamp, which doesn't seem cricket to me.

@jeffkaufman

This comment has been minimized.

Copy link
Owner Author

jeffkaufman commented Jan 10, 2019

@TheJhyde

You'd have to edit the merge timestamp, which doesn't seem cricket to me.

This PR uses the timestamps github provides, which I think come from GitHub's internal records and not from git.

@TheJhyde

This comment has been minimized.

Copy link
Contributor

TheJhyde commented Jan 10, 2019

Yes, the PR prevents any kind of chicanery from git timestamps. I had been delaying approving it up until now because I'd hoped to engage in some of that chicanery.

@pavellishin

This comment has been minimized.

Copy link
Collaborator

pavellishin commented Jan 10, 2019

That would have been a beautiful way to win, tbh.

@jeffkaufman jeffkaufman merged commit 5fcbf51 into master Jan 11, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment