src/Pure/Tools/server.scala
changeset 71747 1dd514c8c1df
parent 71726 a5fda30edae2
child 72163 f5722290a4d0
--- a/src/Pure/Tools/server.scala	Sun Apr 12 21:53:58 2020 +0100
+++ b/src/Pure/Tools/server.scala	Mon Apr 13 16:16:22 2020 +0200
@@ -534,7 +534,7 @@
     for ((_, session) <- sessions) {
       try {
         val result = session.stop()
-        if (!result.ok) log("Session shutdown failed: return code " + result.rc)
+        if (!result.ok) log("Session shutdown failed: " + result.print_rc)
       }
       catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
     }