From d51f7f2770858713204b7e670119090a26c9f194 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 27 Mar 2019 23:20:29 -0400
Subject: Don't escape slashes for JSON

---
 lib/ur/json.ur | 1 -
 1 file changed, 1 deletion(-)

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
-- 
cgit v1.2.3