Custom PR string for combinatorial-games repo

Stream: Zulip meta

[Violeta Hernández]

Is there a chance we could make CGT#123 redirect to https://github.com/vihdzp/combinatorial-games/pull/123 ?

[Violeta Hernández]

(There's probably someone specific I need to ask, but I don't know who it is)

[Robin Arnez]

See #Zulip meta > PhysLean linkifier broken @ 💬 for discussion about this

[Robin Arnez]

So basically anyone that has access to the organisation settings should be able to add a linkifier

[Bryan Gin-ge Chen]

I've just done this; feel free to open a thread in #Zulip meta for other requests like this (there might already be an existing thread for linkifiers there).

[Notification Bot]

This topic was moved here from #general > Custom PR string for combinatorial-games repo by Bryan Gin-ge Chen.

[Violeta Hernández]

Could we also get a docs linkifier as well, for https://vihdzp.github.io/combinatorial-games ?

[Violeta Hernández]

To be more explicit, I'd like something like LeanAPAP#conv that links to the docs (if I try CGT#Nimber it doesn't currently do this). @Bryan Gin-ge Chen

[Bryan Gin-ge Chen]

Done! test: CGT#Nimber

[Violeta Hernández]

Thanks!