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,