changeset 71684 | 5036edb025b7 |
parent 71601 | 97ccf48c2f0c |
child 71685 | d5773922358d |
--- a/src/Pure/Tools/server.scala Sat Apr 04 18:05:37 2020 +0200 +++ b/src/Pure/Tools/server.scala Sat Apr 04 18:13:05 2020 +0200 @@ -442,7 +442,7 @@ find(db, name) match { case Some(server_info) => using(server_info.connection())(_.write_message("shutdown")) - while(server_info.active) { Thread.sleep(50) } + while(server_info.active) { Time.seconds(0.05).sleep } true case None => false }