Remove pull request timeout
People are submitting perfectly good pull requests. However they get closed and thus wasted if nobody looks at them within a certain amount of time. Therefore that robot should be retired.
Therefore that robot should be retired.
Two things are true.
- I agree the robot should be booted.
- You made a ton of tiny PRs that are going to burn all of our CI minutes, generate a messy log in our history, and have to be sequentially merged one-at-a-time. This is why they're not merged.
Howard
Thanks,
however I'm using the GitHub web interface.
Okay. I won't submit any more.
I just hope the system won't throw away the ones that I submitted.
however I'm using the GitHub web interface.
oh!
I wondered why there was all these little commits because if you developing locally on a computer you definitely wouldn't do it that way.
I volunteer to merge this all up for you.
Super! And sorry about your CI minutes. Today's the first time I realized there were such things.
I believe you can use the web interface to combine several commits to a new branch. Once you've accumulated enough changes into one branch, then you'd submit that branch for a single PR. Also, use the "latest" version to find edits so they are targeted for master. We'll need to (probably) cherry-pick these from 9.2 to master, which I can do later today.
As for removing PR timeout, I'm neutral on it, and could be convinced to remove it, or modify it to some sort-of reminder alert for further action (rather than slamming the door closed).
I think there's many still left you didn't find. He's just one page,
As far as combining things using the GitHub interface...
Well if I wasn't so intellectually challenged, I wouldn't be using that interface in the first place..
And there's a four out of five possibility that I would create an even bigger mess.
But anyway I'm happy not to be messing with those PRs anymore, I'll just describe future problems via a bug report (issue).
yes, all those PRs should now be closed. Every thing should be in #3858
I hope you mean you tried to close all the ones you found.
And that you're not trying to tell me to go close them.
Because there's plenty more open ones, whose last comment was made by the robot.
I mean it's rather hard for me to tell today on this tiny cell phone, if something should have been closed or not.
I guess please just go to the open pull request category, and look for anything by user:jidanni, and close anything that should be closed. Thanks!
(I see! The GitHub notification summary page just makes it look like The last action was that of the robot. But clicking on a random item shows indeed there were other actions too!)
2. You made a ton of tiny PRs that are going to burn all of our CI minutes
You'd better mark them as [ci skip] in the commit message. That's what it is invented for. See also:
- GitHub Actions: https://github.blog/changelog/2021-02-08-github-actions-skip-pull-request-and-push-workflows-with-skip-ci/
- Travis CI: https://docs.travis-ci.com/user/customizing-the-build/#skipping-a-build
- Appveyor: https://www.appveyor.com/docs/how-to/filtering-commits/#skip-directive-in-commit-message
- Cirrus CI: https://cirrus-ci.org/guide/writing-tasks/#conditional-task-execution
You'd better mark them as
[ci skip]in the commit message
true, but it must only be used for really trivial changes, like a typo. Anything more involved related to documentation has the risk of having some minor issue like wrong indentation, or lacking some backquote character, etc, which eventually breaks the doc build.