src/Pure/Tools/server.scala
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
         }