# HG changeset patch
# User wenzelm
# Date 1521150119 -3600
# Node ID e4e740ba74a479f253f288b689a6fb6b518427bf
# Parent  39b27d38a54ccc28eefc49549f8cbcfd320a1ed8
tuned message -- more readable JSON;

diff -r 39b27d38a54c -r e4e740ba74a4 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Thu Mar 15 22:28:20 2018 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 15 22:41:59 2018 +0100
@@ -479,7 +479,7 @@
     _sessions.change_result(sessions =>
       sessions.get(id) match {
         case Some(session) => (session, sessions - id)
-        case None => error("No session " + quote(id))
+        case None => error("No session " + Library.single_quote(id))
       })
   }