src/Pure/Tools/server_commands.scala

--- a/src/Pure/Tools/server_commands.scala	Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala	Mon Apr 13 16:16:22 2020 +0200
@@ -86,7 +86,10 @@
               }))
 
       if (results.ok) (results_json, results, options, base_info)
-      else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
+      else {
+        throw new Server.Error("Session build failed: " + Process_Result.print_rc(results.rc),
+          results_json)
+      }
     }
   }
 
@@ -136,7 +139,7 @@
       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)
+      else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json)
     }
   }