| Sat, 25 May 2024 19:42:09 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 24 May 2024 17:14:02 +0200 |
wenzelm |
proper SSH.System operation;
|
file |
diff |
annotate
|
| Fri, 24 May 2024 17:06:57 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 24 May 2024 16:15:27 +0200 |
wenzelm |
more uniform/robust detect_repository/is_repository: actually check hg root;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 14:48:11 +0100 |
wenzelm |
performance tuning: cache graph;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2023 21:11:59 +0200 |
wenzelm |
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 12:53:28 +0200 |
wenzelm |
misc tuning: support "scalac -source 3.3";
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 22:55:01 +0200 |
wenzelm |
more direct hg_sync init via ssh (see also 721b3278c8e4);
|
file |
diff |
annotate
|
| Sat, 08 Apr 2023 20:21:30 +0200 |
wenzelm |
more options;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2023 19:32:09 +0200 |
wenzelm |
use "rsync --secluded-args" by default, discontinue obsolete option -P of sync tools;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2023 17:20:15 +0200 |
wenzelm |
clarified signature: more abstract;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2023 16:59:20 +0200 |
wenzelm |
tuned signature;
|
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
|
| Sat, 08 Apr 2023 10:24:54 +0200 |
wenzelm |
clarified signature: avoid object-oriented "dispatch";
|
file |
diff |
annotate
|
| Sun, 05 Mar 2023 15:34:00 +0100 |
wenzelm |
clarified signature: manage "verbose" flag via "progress";
|
file |
diff |
annotate
|
| Fri, 24 Feb 2023 20:40:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 16:29:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2023 15:42:25 +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
|
| Wed, 30 Nov 2022 15:03:31 +0100 |
wenzelm |
clarified signature: prefer Scala functions instead of shell scripts;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2022 14:26:42 +0200 |
wenzelm |
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
|
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 10:34:52 +0200 |
wenzelm |
clarified command-line;
|
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
|
| Fri, 12 Aug 2022 16:01:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 13 Jun 2022 11:48:46 +0200 |
wenzelm |
clarified options of "isabelle hg_sync" vs. "isabelle sync";
|
file |
diff |
annotate
|
| Tue, 07 Jun 2022 19:23:31 +0200 |
wenzelm |
avoid noise via context.progress (amending 68162e4f60a7);
|
file |
diff |
annotate
|
| Tue, 07 Jun 2022 19:13:56 +0200 |
wenzelm |
tuned whitespace;
|
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
|
| Mon, 06 Jun 2022 19:28:02 +0200 |
wenzelm |
avoid redundant meta data: exclude .hg_archival.txt;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2022 20:14:59 +0200 |
wenzelm |
more meta data;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2022 19:19:55 +0200 |
wenzelm |
provide .hg_sync meta data;
|
file |
diff |
annotate
|
| Sat, 04 Jun 2022 16:54:24 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2022 10:10:42 +0200 |
wenzelm |
clarified options;
|
file |
diff |
annotate
|
| Tue, 31 May 2022 22:10:48 +0200 |
wenzelm |
clarified signature (again);
|
file |
diff |
annotate
|
| Tue, 31 May 2022 16:01:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 31 May 2022 13:14:46 +0200 |
wenzelm |
support explicit SSH port;
|
file |
diff |
annotate
|
| Mon, 30 May 2022 11:51:34 +0200 |
wenzelm |
clarified option -T;
|
file |
diff |
annotate
|
| Mon, 30 May 2022 11:02:13 +0200 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Mon, 30 May 2022 10:52:00 +0200 |
wenzelm |
clarified command-line options;
|
file |
diff |
annotate
|
| Mon, 30 May 2022 10:31:56 +0200 |
wenzelm |
support thorough check of file content;
|
file |
diff |
annotate
|
| Sun, 29 May 2022 23:49:58 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 29 May 2022 21:32:28 +0200 |
wenzelm |
more robust: local repository required;
|
file |
diff |
annotate
|
| Sun, 29 May 2022 20:57:10 +0200 |
wenzelm |
support option -r;
|
file |
diff |
annotate
|
| Sun, 29 May 2022 17:26:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 29 May 2022 16:25:37 +0200 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| Sun, 29 May 2022 15:16:49 +0200 |
wenzelm |
support filter rules, notably "protect";
|
file |
diff |
annotate
|
| Sun, 29 May 2022 13:13:45 +0200 |
wenzelm |
support for "isabelle hg_sync";
|
file |
diff |
annotate
|
| Sun, 29 May 2022 11:45:32 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 28 May 2022 22:33:11 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 23:19:12 +0200 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Sun, 16 May 2021 13:34:27 +0200 |
wenzelm |
tuned signature --- following hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Tue, 04 May 2021 12:54:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2021 22:39:33 +0200 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|