# HG changeset patch
# User wenzelm
# Date 1521651317 -3600
# Node ID a7731d581bbc4ff0f625c550eb79e4c7e7887051
# Parent  3cda747493d8049d8d26b02217574dd4f1b47ae9
clarified result;

diff -r 3cda747493d8 -r a7731d581bbc src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Wed Mar 21 13:17:30 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Wed Mar 21 17:55:17 2018 +0100
@@ -89,14 +89,19 @@
 
       val results_json =
         JSON.Object(
+          "ok" -> results.ok,
           "return_code" -> results.rc,
           "sessions" ->
             results.sessions.toList.sortBy(sessions_order).map(session =>
-              JSON.Object(
-                "session" -> session,
-                "return_code" -> results(session).rc,
-                "timeout" -> results(session).timeout,
-                "timing" -> results(session).timing.json)))
+              {
+                val result = results(session)
+                JSON.Object(
+                  "session" -> session,
+                  "ok" -> result.ok,
+                  "return_code" -> result.rc,
+                  "timeout" -> result.timeout,
+                  "timing" -> result.timing.json)
+              }))
 
       if (results.ok) (results_json, results, base_info)
       else throw new Server.Error("Session build failed: return code " + results.rc, results_json)