Why is '
classified as a special character in string_syntax.ML
and therefore not printed as e.g. STR ''won't''
?
It has a special meaning as an escape character when you define user-space syntax but I have no idea whether that is related.
Last updated: Dec 07 2024 at 16:22 UTC