src/Pure/General/rsync.scala
Sat, 01 Jun 2024 16:19:14 +0200 wenzelm tuned;
Fri, 24 May 2024 19:15:51 +0200 wenzelm clarified signature;
Fri, 14 Apr 2023 22:55:01 +0200 wenzelm more direct hg_sync init via ssh (see also 721b3278c8e4);
Sat, 08 Apr 2023 20:21:30 +0200 wenzelm more options;
Sat, 08 Apr 2023 19:34:51 +0200 wenzelm tuned comments;
Sat, 08 Apr 2023 19:32:09 +0200 wenzelm use "rsync --secluded-args" by default, discontinue obsolete option -P of sync tools;
Sat, 08 Apr 2023 19:02:51 +0200 wenzelm tuned output;
Sat, 08 Apr 2023 18:59:58 +0200 wenzelm misc tuning and clarification;
Sat, 08 Apr 2023 18:08:20 +0200 wenzelm use remote copy of locally installed rsync component: for uniform version and options;
Sat, 08 Apr 2023 17:20:15 +0200 wenzelm clarified signature: more abstract;
Sat, 08 Apr 2023 16:58:01 +0200 wenzelm more direct Hg_Sync.check_directory via SSH operations;
Sat, 08 Apr 2023 16:37:54 +0200 wenzelm clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
Sun, 05 Mar 2023 15:34:00 +0100 wenzelm clarified signature: manage "verbose" flag via "progress";
Sun, 05 Mar 2023 15:25:02 +0100 wenzelm tuned;
Fri, 24 Feb 2023 20:52:35 +0100 wenzelm tuned;
Sun, 11 Dec 2022 12:52:46 +0100 wenzelm clarified signature;
Sun, 11 Dec 2022 11:47:28 +0100 wenzelm tuned signature;
Fri, 16 Sep 2022 14:57:48 +0200 wenzelm clarified modules;
Tue, 13 Sep 2022 11:56:38 +0200 wenzelm let rsync re-use ssh connection via control path;
Tue, 13 Sep 2022 09:59:08 +0200 wenzelm clarified default: do not override port from ssh_config, which could be different from 22;
Sat, 11 Jun 2022 20:45:14 +0200 wenzelm more comments;
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;
Tue, 07 Jun 2022 17:22:17 +0200 wenzelm clarified context with global defaults;
Tue, 07 Jun 2022 17:10:51 +0200 wenzelm tuned signature;
Tue, 07 Jun 2022 17:07:10 +0200 wenzelm clarified signature: more explicit type Rsync.Context;
Tue, 07 Jun 2022 16:47:57 +0200 wenzelm clarified signature;
Tue, 07 Jun 2022 12:32:53 +0200 wenzelm clarified modules;
less more (0) tip