Zulip Chat Archive

Stream: PR reviews

Topic: topic names


view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Scott Olson (Oct 07 2018 at 11:41):

Docs are at https://zulipchat.com/help/add-a-custom-linkification-filter

view this post on Zulip Mario Carneiro (Oct 07 2018 at 11:56):

testing: #123, lean#123

view this post on Zulip Scott Morrison (Oct 07 2018 at 11:56):

Nice!

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 07 2018 at 11:57):

PRs and issues are in the same namespace (numberspace)

view this post on Zulip Mario Carneiro (Oct 07 2018 at 11:58):

you will notice that issue #123 I linked to is actually a PR

view this post on Zulip Scott Morrison (Oct 07 2018 at 12:06):

Great.

view this post on Zulip 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: May 07 2021 at 19:12 UTC