b706c0064e
this didn’t recognize the new comments with an intro, and thus the bot would post multiple comments. The code was also out of sync with mathlib, fixing. The `first(…)` in the `jq` program makes it more robust in case this went wrong once (as on #3171) and there are now multiple PRs matching. |
||
|---|---|---|
| .. | ||
| ISSUE_TEMPLATE | ||
| workflows | ||
| PULL_REQUEST_TEMPLATE.md | ||