leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

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: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll