Allowed characters in doc URLs

Stream: mathlib4

[Violeta Hernández]

I recently noticed that the URL in docs#LanderParkinSelfridgeConjecture was not formatted properly in the docs. That URL has commas, and docgen splits URLs at such characters. I opened #32556 to replace them with ASCII escapes, but got told that I should be discussed on Zulip.

Personally I do believe splitting at punctuation marks makes more sense than not (since otherwise writing https://example.com, would then lead to an incorrect link). Wonder what others think.

[Kim Morrison]

ASCII escapes sound good to me.

[Anthony Wang]

It seems slightly inelegant to have escape characters (technically it's URL encoding, not ASCII escapes), so maybe a more complicated solution could be to have docgen split on whitespace, and then trim punctuation from the end of links.

[Eric Wieser]

"doc-gen" here is just markdown