aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@csail.mit.edu>2018-08-17 09:37:11 -0400
committerGravatar GitHub <noreply@github.com>2018-08-17 09:37:11 -0400
commit0e41b2ab9485f46c4303be46d41e39203eeb7138 (patch)
treea51ac69b0ac1e47829a30d749bfadcf4f7a9f607
parent24cb4d7ac2fa5fb8b5af511f05ed9a673b6f35ec (diff)
parent8bdd29f65c57570776f0c9f90d75f7818b0cdaa6 (diff)
Merge pull request #134 from steinuil/json-single-quote
removed invalid JSON escape character
-rw-r--r--lib/ur/json.ur2
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>)