Stream: coqbot devs & users

Topic: backports

Enrico Tassi (Nov 19 2020 at 13:10):

I did just git push upstream somehash:v8.13 and coqbot did not move cards (eg see 12653). What did I do wrong?

Théo Zimmermann (Nov 19 2020 at 16:29):

In the case of this PR the following happened:

• at some point, you removed the PR from the project, then you added it again
• however, in the meantime, coqbot had automatically considered this was a backport rejection and moved the PR to the 8.14 milestone
• coqbot doesn't have a reverse mechanism, so the PR stayed in the 8.14 milestone
• given that coqbot checks the milestone description to know if it needs to move the PR in a backporting project, it didn't do anything for this PR

Théo Zimmermann (Nov 19 2020 at 16:29):

I'll fix this case manually. Are there other PRs that are impacted?

Enrico Tassi (Nov 19 2020 at 16:35):

No, I think I removed only 2 by mistake

Last updated: May 28 2023 at 18:29 UTC