mathlib3
9407a363 - ci(*): tweak synchronization bot behavior (#17693)

Commit
3 years ago
ci(*): tweak synchronization bot behavior (#17693) This changes the script to output a list of filenames and PR links, so that a quick scan on github can verify that the PR numbers are entered correctly in the yaml. This also changes the user doing the committing to be the community user.
Author
Parents
Loading