Zulip Chat Archive
Stream: PR reviews
Topic: topic names
Johan Commelin (Oct 07 2018 at 11:36):
Can we have slightly more descriptive topic names please? Currently they are just hash-number, and they actually link to issues of the lean repo instead of mathlib...
Scott Olson (Oct 07 2018 at 11:39):
An organization admin could modify the linkification filter for topic names to point those to mathlib, or make lean#123 and mathlib#123 work as topic names with auto-linking
Scott Olson (Oct 07 2018 at 11:41):
Docs are at https://zulipchat.com/help/add-a-custom-linkification-filter
Mario Carneiro (Oct 07 2018 at 11:56):
Scott Morrison (Oct 07 2018 at 11:56):
Nice!
Scott Morrison (Oct 07 2018 at 11:57):
Is there an easy way to link to PRs, since we use them more than issues anyway?
Mario Carneiro (Oct 07 2018 at 11:57):
PRs and issues are in the same namespace (numberspace)
Mario Carneiro (Oct 07 2018 at 11:58):
you will notice that issue #123 I linked to is actually a PR
Scott Morrison (Oct 07 2018 at 12:06):
Great.
Scott Olson (Oct 07 2018 at 12:20):
The topic named #397 still has the wrong link but I suspect it would update if renamed and then renamed back
Last updated: Dec 20 2023 at 11:08 UTC