bot icon indicating copy to clipboard operation
bot copied to clipboard

coqbot minimization should mention Issue # in commit, not just "Added user script in coqbot.sh"

Open JasonGross opened this issue 4 years ago • 1 comments

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.

JasonGross avatar Jul 08 '21 14:07 JasonGross

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.

Zimmi48 avatar Jul 08 '21 14:07 Zimmi48