Zulip Chat Archive
Stream: general
Topic: long lines & URLs
Yury G. Kudryashov (Jun 29 2020 at 14:28):
Is there any reasonable way to add a link with a long URL without breaking the "100 chars" limit?
Yury G. Kudryashov (Jun 29 2020 at 14:28):
https://github.com/leanprover-community/mathlib/pull/3172/files#r447012958
Johan Commelin (Jun 29 2020 at 14:29):
Just break the limit. nobody is interested in reading the url anyways...
Johan Commelin (Jun 29 2020 at 14:29):
As in the literal url, they might be interested in reading what it points to, but that's not what I'm talking about
Mario Carneiro (Jun 29 2020 at 14:30):
Does the "footnote style" for inline links work? You could use that
Last updated: Dec 20 2023 at 11:08 UTC