author | wenzelm |
Fri, 09 Mar 2018 13:03:55 +0100 | |
changeset 67790 | 1babcc248be0 |
parent 67789 | 77a65c9a849a |
child 67791 | acecef5fad58 |
--- a/src/Pure/Tools/server.scala Fri Mar 09 12:45:53 2018 +0100 +++ b/src/Pure/Tools/server.scala Fri Mar 09 13:03:55 2018 +0100 @@ -134,6 +134,7 @@ stmt.execute() }) + server.start (entry, Some(server)) } }) @@ -258,6 +259,8 @@ } } + def start { server_thread } + def join { server_thread.join; shutdown() } def shutdown() { server_socket.close }