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