equal
deleted
inserted
replaced
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Rsync { |
10 object Rsync { |
11 sealed case class Context(progress: Progress, port: Int = SSH.default_port) { |
11 sealed case class Context(progress: Progress, |
|
12 port: Int = SSH.default_port, |
|
13 archive: Boolean = true, |
|
14 protect_args: Boolean = true |
|
15 ) { |
12 def command: String = |
16 def command: String = |
13 "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) |
17 "rsync --rsh=" + Bash.string("ssh -p " + port) + |
|
18 (if (archive) " --archive" else "") + |
|
19 (if (protect_args) " --protect-args" else "") |
14 } |
20 } |
15 |
21 |
16 def exec( |
22 def exec( |
17 context: Context, |
23 context: Context, |
18 verbose: Boolean = false, |
24 verbose: Boolean = false, |