--- a/src/Pure/Tools/server_commands.scala Wed Mar 21 21:31:16 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Wed Mar 21 21:31:40 2018 +0100
@@ -153,7 +153,7 @@
def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
{
val result = session.stop()
- val result_json = JSON.Object("return_code" -> result.rc)
+ val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
if (result.ok) (result_json, result)
else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)