--- 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)