json report backslash escapes

[sheckman16]

It would be convenient if unit names containing backslashes (like "##/") escaped the backslashes in json. I wish for
"name": "\\##/ (2918)"
instead of the present encoding, which is
"name": "\##/ (2918)"

I wish for this because the default python json decoder chokes on the existing report.

[Mochnant]

That's actually a forward slash, not a backslash, which isn't required to be escaped in the json specification, but it is permitted to be if useful.

[sheckman16]

I suspect github formatting is making the four character name you see different than the four characters I typed. Let me try again, without trying to enter any "reverse solidus" characters in my comment.

The troublesome name consists of the four characters, ascii 92, ascii 35, ascii 35, ascii 47. In order, I would name these "backslash", "octothorpe", "octothorpe", "forward slash". RFC 8259 names ascii 92 "reverse solidus", and ascii 47 "solidus".

RFC 8259 reads:

All Unicode characters may be placed within the
quotation marks, except for the characters that MUST be escaped:
quotation mark, reverse solidus, and the control characters (U+0000
through U+001F).

The problem with the four character name of unit 2918 is the first character, ascii 92. Python's json decoder, following RFC 8259, thinks ascii 92 (the reverse solidus) must be escaped, so interprets ascii 92 followed by ascii 35 in the JSON as the undefined escape sequence "(reverse solidus)(octothorpe)".