# HG changeset patch
# User wenzelm
# Date 1521664300 -3600
# Node ID a72f01c63262a59f4e834b79d27d1b9b0e6129c0
# Parent  d827728b74b3399a608e8355db927dcce62b4bd3
clarified result;

diff -r d827728b74b3 -r a72f01c63262 src/Pure/Tools/server_commands.scala
--- 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)