author | wenzelm |
Wed, 14 Sep 2022 23:58:26 +0200 | |
changeset 76159 | 361cfb8e3648 |
parent 76158 | 0302bdf63a08 |
child 76160 | 23c513c192ac |
--- a/src/Pure/General/ssh.scala Wed Sep 14 23:09:02 2022 +0200 +++ b/src/Pure/General/ssh.scala Wed Sep 14 23:58:26 2022 +0200 @@ -146,7 +146,7 @@ } def run_scp(opts: String = "", args: String = ""): Process_Result = { - val opts1 = "-s -p -q" + (if (opts.nonEmpty) " " + opts else "") + val opts1 = "-p -q" + (if (opts.nonEmpty) " " + opts else "") run_command("scp", opts = opts1, args = args) }