# HG changeset patch
# User wenzelm
# Date 1628364347 -7200
# Node ID bba35ad317abeb39a429244f01f2399efe7a6e7c
# Parent  8a5e02ef975c443b94788ff1b254ae73a647d13c
tuned signature;

diff -r 8a5e02ef975c -r bba35ad317ab src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/ML/ml_console.scala	Sat Aug 07 21:25:47 2021 +0200
@@ -75,8 +75,8 @@
               options, logic, dirs = dirs, include_sessions = include_sessions).check.base))
 
       POSIX_Interrupt.handler { process.interrupt() } {
-        new TTY_Loop(process.stdin, process.stdout).join
-        val rc = process.join
+        new TTY_Loop(process.stdin, process.stdout).join()
+        val rc = process.join()
         if (rc != 0) sys.exit(rc)
       }
     }
diff -r 8a5e02ef975c -r bba35ad317ab src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/PIDE/prover.scala	Sat Aug 07 21:25:47 2021 +0200
@@ -110,7 +110,7 @@
 
   private val process_result: Future[Process_Result] =
     Future.thread("process_result") {
-      val rc = process.join
+      val rc = process.join()
       val timing = process.get_timing
       Process_Result(rc, timing = timing)
     }
diff -r 8a5e02ef975c -r bba35ad317ab src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/System/bash.scala	Sat Aug 07 21:25:47 2021 +0200
@@ -183,9 +183,9 @@
 
     // join
 
-    def join: Int =
+    def join(): Int =
     {
-      val rc = proc.waitFor
+      val rc = proc.waitFor()
       do_cleanup()
       rc
     }
@@ -218,7 +218,7 @@
         }
 
       val rc =
-        try { join }
+        try { join() }
         catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
 
       watchdog_thread.foreach(_.cancel())
diff -r 8a5e02ef975c -r bba35ad317ab src/Pure/System/tty_loop.scala
--- a/src/Pure/System/tty_loop.scala	Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/System/tty_loop.scala	Sat Aug 07 21:25:47 2021 +0200
@@ -62,7 +62,7 @@
     catch { case e: IOException => case Exn.Interrupt() => }
   }
 
-  def join: Unit = { console_output.join; console_input.join }
+  def join(): Unit = { console_output.join; console_input.join }
 
   def cancel(): Unit = console_input.cancel()
 }
diff -r 8a5e02ef975c -r bba35ad317ab src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Aug 07 19:58:38 2021 +0200
+++ b/src/Pure/Tools/server.scala	Sat Aug 07 21:25:47 2021 +0200
@@ -508,7 +508,7 @@
           init(name, port = port, existing_server = existing_server, log = log)
         Output.writeln(server_info.toString, stdout = true)
         if (console) {
-          using(server_info.connection())(connection => connection.tty_loop().join)
+          using(server_info.connection())(connection => connection.tty_loop().join())
         }
         server.foreach(_.join())
       }