clarified result;
authorwenzelm
Wed Mar 21 21:31:40 2018 +0100 (14 months ago)
changeset 67916a72f01c63262
parent 67915 d827728b74b3
child 67917 d13b2dd20f5e
clarified result;
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/Tools/server_commands.scala	Wed Mar 21 21:31:16 2018 +0100
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Wed Mar 21 21:31:40 2018 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4      def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
     1.5      {
     1.6        val result = session.stop()
     1.7 -      val result_json = JSON.Object("return_code" -> result.rc)
     1.8 +      val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
     1.9  
    1.10        if (result.ok) (result_json, result)
    1.11        else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)