Summary
- clarified server shutdown: stop all sessions;
- more explicit error messages; clarified signature;
- more explicit errors; tuned;
The file was modified | src/Pure/Tools/server.scala (diff) |
The file was modified | src/Pure/Tools/server.scala (diff) |
The file was modified | src/Pure/Tools/server_commands.scala (diff) |
The file was modified | src/Pure/Tools/server_commands.scala (diff) |