Zulip Chat Archive
Stream: general
Topic: auto links to github
Johan Commelin (Mar 13 2019 at 16:00):
If we type #816 #816 we get a link to github. Technically it no longer points to the correct repo. Not a big deal, because a forward saves us. We still might want to fix it. @Mario Carneiro @Simon Hudon
Mario Carneiro (Mar 13 2019 at 16:05):
link #816
Johan Commelin (Mar 13 2019 at 16:15):
@Mario Carneiro Merci!
Last updated: Dec 20 2023 at 11:08 UTC