MAINTENANCE. Cleaning up stale PRs. #14495
Conversation
Closing the following PRs due to requests or unresponsive users. Closes apache#13923 Closes apache#14462 Closes apache#13123 Closes apache#14423 (requested by srowen) Closes apache#14424 (requested by srowen) Closes apache#14101 (requested by jkbradley) Closes apache#10676 (requested by srowen) Closes apache#10943 (requested by yhuai) Closes apache#9936 Closes apache#10701
|
Let me know if there are any concerns. |
|
Also going to add #10474. |
|
Adding #13248 |
|
Adding #14347 |
|
Adding #10356 |
|
Adding #9866 |
|
Test build #63230 has finished for PR 14495 at commit
|
|
Does just mentioning the numbers in comments cause them to close when this merges? I wasn't sure whether the bot or Github looks for "closes ...". Here are some more on my list: Closes #14310 |
|
No, just mentioning in comments doesn't work. I'm adding the "Closes #foo" text to the commit message I'll push, and at that time github will close them. I'll look at adding the ones on your list. |
|
I'll let 10270 since the submitter is active (I'll let him close the PR if he can't fix it). I'll take a look at 14232 since I've played with that code (it's just a comment anyway). |
|
Alright, commit is pushed, lots of PRs are in the process of being closed. |
3 participants
Closing the following PRs due to requests or unresponsive users.
Closes #13923
Closes #14462
Closes #13123
Closes #14423 (requested by srowen)
Closes #14424 (requested by srowen)
Closes #14101 (requested by jkbradley)
Closes #10676 (requested by srowen)
Closes #10943 (requested by yhuai)
Closes #9936
Closes #10701