bot
bot copied to clipboard
coqbot minimization should mention Issue # in commit, not just "Added user script in coqbot.sh"
Currently when a user initiates (non-ci) minimization, the commit message is just "Added user script in coqbot.sh". It should be something like "Added user script from coq/coq#<ISSUE #> in coqbot.sh" and should ideally include a link to the particular comment in the body of the commit message.
We can get the URL of the comment directly from the webhook (under comment / html_url). The simplest solution would likely to add this to the webhook parsing, pass this around in function calls, and include it in the commit message.