search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
26 stars 11 forks source link

doubling underscores in URLs #128

Closed jkingdon closed 1 year ago

jkingdon commented 1 year ago

metamath-knife produces an error on the following:

    $( A singleton is linearly independent iff it does not contain a torsion
       element.  According to Wikipedia ("Torsion (algebra)", 15-Apr-2019,
       ~ https://en.wikipedia.org/wiki/Torsion_(algebra) ):  "An element m of a

The error is:

warning: Invalid escape character
      --> set.mm:740600:47
       |
740600 |        ~ https://en.wikipedia.org/wiki/Torsion_(algebra) ):  "An element m of a
       |                                               - This escape character should be doubled
       |
       = note: This character has special meaning in this position, but it was not interpretable here.
       = note: Use ~~ or [[ or `` if you mean to include the character literally

However, underscores don't need to be doubled in URLs, do they? At least, if I use the metamath-exe SHOW STATEMENT/ALT_HTML to produce a web page, the undoubled underscore turns into an underscore here, and the doubled underscore turns into a doubled underscore (which is not what we want).

tirix commented 1 year ago

According to @digama0's comment in #129, basically, underscores in URLs should be doubled. Then this would not be an issue.