Sat, 08 Apr 2023 19:02:51 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
Sat, 08 Apr 2023 18:59:58 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
Sat, 08 Apr 2023 18:08:20 +0200 |
wenzelm |
use remote copy of locally installed rsync component: for uniform version and options;
|
file |
diff |
annotate
|
Sat, 08 Apr 2023 17:20:15 +0200 |
wenzelm |
clarified signature: more abstract;
|
file |
diff |
annotate
|
Sat, 08 Apr 2023 16:58:01 +0200 |
wenzelm |
more direct Hg_Sync.check_directory via SSH operations;
|
file |
diff |
annotate
|
Sat, 08 Apr 2023 16:37:54 +0200 |
wenzelm |
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
|
file |
diff |
annotate
|
Sun, 05 Mar 2023 15:34:00 +0100 |
wenzelm |
clarified signature: manage "verbose" flag via "progress";
|
file |
diff |
annotate
|
Sun, 05 Mar 2023 15:25:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 24 Feb 2023 20:52:35 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 11 Dec 2022 12:52:46 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Sun, 11 Dec 2022 11:47:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 16 Sep 2022 14:57:48 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 13 Sep 2022 11:56:38 +0200 |
wenzelm |
let rsync re-use ssh connection via control path;
|
file |
diff |
annotate
|
Tue, 13 Sep 2022 09:59:08 +0200 |
wenzelm |
clarified default: do not override port from ssh_config, which could be different from 22;
|
file |
diff |
annotate
|
Sat, 11 Jun 2022 20:45:14 +0200 |
wenzelm |
more comments;
|
file |
diff |
annotate
|
Tue, 07 Jun 2022 17:47:28 +0200 |
wenzelm |
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
|
file |
diff |
annotate
|
Tue, 07 Jun 2022 17:22:17 +0200 |
wenzelm |
clarified context with global defaults;
|
file |
diff |
annotate
|
Tue, 07 Jun 2022 17:10:51 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 07 Jun 2022 17:07:10 +0200 |
wenzelm |
clarified signature: more explicit type Rsync.Context;
|
file |
diff |
annotate
|
Tue, 07 Jun 2022 16:47:57 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Tue, 07 Jun 2022 12:32:53 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|