author | wenzelm |
Thu, 15 Mar 2018 22:41:59 +0100 | |
changeset 67873 | e4e740ba74a4 |
parent 67872 | 39b27d38a54c |
child 67874 | 599753dd6501 |
--- 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)) }) }