src/Pure/General/ssh.scala
changeset 80235 06036a16779f
parent 80229 5e32da8238e1
child 80441 c420429fdf4c
--- a/src/Pure/General/ssh.scala	Sat Jun 01 16:26:35 2024 +0200
+++ b/src/Pure/General/ssh.scala	Sat Jun 01 21:49:50 2024 +0200
@@ -567,7 +567,7 @@
         input: String = "",
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
-        watchdog: Option[Bash.Watchdog] = None,
+        watchdog: Bash.Watchdog = Bash.Watchdog.none,
         redirect: Boolean = false,
         settings: Boolean = true,
         strict: Boolean = true,