# HG changeset patch
# User wenzelm
# Date 1520957600 -3600
# Node ID 7f82445e8f0e1ef63238eccc0e284ae02ebf12d5
# Parent  ff561f6e0a8e2b0131b46d830a3c779aba1d83b7
tuned;

diff -r ff561f6e0a8e -r 7f82445e8f0e src/Pure/Admin/remote_dmg.scala
--- a/src/Pure/Admin/remote_dmg.scala	Tue Mar 13 16:08:13 2018 +0100
+++ b/src/Pure/Admin/remote_dmg.scala	Tue Mar 13 17:13:20 2018 +0100
@@ -56,7 +56,7 @@
             case _ => getopts.usage()
           }
 
-        val options = Options.init
+        val options = Options.init()
         using(SSH.open_session(options, host = host, user = user, port = port))(
           remote_dmg(_, tar_gz_file, dmg_file, volume_name))
       }