Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
github-ircbot should support "topic: GitHubURL" as alias of "github topic: GitHubURL" #50
The wgmeeting-github-ircbot should support the syntax:
where GitHubURL is a URL that starts with https://github.com/ ... and ends with a number segment (optional # fragment), just as it currently supports the "github topic: GitHubURL" syntax, because it is easier to remember, and 100% of past uses of "topic: GitHubURL" were clearly intended to do just that, and had to be unnecessarily followed up by a redundant "github topic: GitHubURL" command.
E.g. from the #css IRC log search results:
Note that this is a very precise request for what to allow, with the text after "Topic: " immediately being an https://github.com/ URL without anything else preceding, and ending with a URL segment that is a number, to avoid errant use of other GitHub URLs.
Given that level of precision, this reflects existing attempted use in the logs 100%, and is sufficiently guarded against false positives, at least from the past ~4 years of history in the logs.
(Originally published at: https://tantek.com/2020/050/b1/)
This was supported in my initial version of the bot, but it was one of the first things I had to remove when it was used in a live CSS WG meeting, in 8379709.
Fundamentally, I think this is because there are two separate things that need to happen:
There's a tendency to frequently correct the second one. But if the normal way of doing the second one involves also doing the first one, then any corrections to the second (since people will just use the usual command that they're used to) will also lead to a boundary, which will then lead to incorrect results: the single topic split into multiple pieces, where some of those pieces get posted to the wrong github issue or to no github issue at all.
The use of
I'd like to do what's in #45 instead of what's here.
Another possibility (instead of or in addition to #45) would be integrating the correct commands for this bot into Zakim's agenda management features, or integrating similar agenda management features into this bot.