# HG changeset patch
# User wenzelm
# Date 1663192706 -7200
# Node ID 361cfb8e36482056ca0be88cad5796f0121c7617
# Parent  0302bdf63a0851407df071efb958d287d8fc82a7
more portable;

diff -r 0302bdf63a08 -r 361cfb8e3648 src/Pure/General/ssh.scala
--- 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)
     }