Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
post_issue_on_zulip.py: various mathlib4 fixes
The bot now posts links to mathlib4 instead of mathlib3. The bot now also posts topic names with the `!4#XXXX` linkifier instead of `#XXXX` (and only searches for topics fitting that pattern). This will save the bot some API calls on topics that are on mathlib3 issues.
- Loading branch information