summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2019-03-27 23:20:29 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2019-03-27 23:20:29 -0400
commitd51f7f2770858713204b7e670119090a26c9f194 (patch)
tree0c9375cc6f8e5093f1ee32b01903c771c9320a3d
parent3f119f5c0a5f210ed442841dfed3ae98786004e9 (diff)
Don't escape slashes for JSON
-rw-r--r--lib/ur/json.ur1
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/ur/json.ur b/lib/ur/json.ur
index 589e81b0..05406739 100644
--- a/lib/ur/json.ur
+++ b/lib/ur/json.ur
@@ -52,7 +52,6 @@ fun escape s =
| #"\t" => "\\t"
| #"\"" => "\\\""
| #"\\" => "\\\\"
- | #"/" => "\\/"
| x => String.str ch
) ^ esc (String.suffix s 1)
end