diff options
author | Adam Chlipala <adamc@csail.mit.edu> | 2018-08-17 09:37:11 -0400 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-17 09:37:11 -0400 |
commit | 0e41b2ab9485f46c4303be46d41e39203eeb7138 (patch) | |
tree | a51ac69b0ac1e47829a30d749bfadcf4f7a9f607 /lib/ur | |
parent | 24cb4d7ac2fa5fb8b5af511f05ed9a673b6f35ec (diff) | |
parent | 8bdd29f65c57570776f0c9f90d75f7818b0cdaa6 (diff) |
Merge pull request #134 from steinuil/json-single-quote
removed invalid JSON escape character
Diffstat (limited to 'lib/ur')
-rw-r--r-- | lib/ur/json.ur | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/lib/ur/json.ur b/lib/ur/json.ur index 817ec16e..589e81b0 100644 --- a/lib/ur/json.ur +++ b/lib/ur/json.ur @@ -51,7 +51,6 @@ fun escape s = | #"\r" => "\\r" | #"\t" => "\\t" | #"\"" => "\\\"" - | #"\'" => "\\\'" | #"\\" => "\\\\" | #"/" => "\\/" | x => String.str ch @@ -101,7 +100,6 @@ fun unescape s = | #"r" => "\r" | #"t" => "\t" | #"\"" => "\"" - | #"\'" => "\'" | #"\\" => "\\" | #"/" => "/" | x => error <xml>JSON unescape: Bad escape char: {[x]}</xml>) |