| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2021 11:52:32 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 26 Jul 2021 13:04:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2021 15:24:04 +0100 |
wenzelm |
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
|
file |
diff |
annotate
|
| Sat, 16 Jan 2021 17:02:14 +0100 |
wenzelm |
clarified return code: re-use SIGALRM for soft timeout;
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 16:51:40 +0100 |
wenzelm |
proper return code for more errors (amending d892f6d66402);
|
file |
diff |
annotate
|
| Sat, 07 Nov 2020 16:36:50 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 15:38:21 +0200 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2020 14:43:02 +0200 |
wenzelm |
more robust protocol for "Timing ..." messages, notably for pide_session=true;
|
file |
diff |
annotate
|
| Mon, 13 Apr 2020 17:40:44 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Mon, 13 Apr 2020 16:32:56 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Mon, 13 Apr 2020 16:16:22 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2020 18:19:46 +0200 |
wenzelm |
clarified signature: more robust;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2020 19:39:11 +0200 |
wenzelm |
more accurate treatment of errors;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2018 19:11:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 06 May 2018 23:01:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 26 Oct 2016 16:04:05 +0200 |
wenzelm |
clarified hg push return code: 1 means "nothing to push";
|
file |
diff |
annotate
|
| Tue, 11 Oct 2016 09:37:59 +0200 |
wenzelm |
eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
|
file |
diff |
annotate
|
| Mon, 03 Oct 2016 20:09:50 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Wed, 09 Mar 2016 14:54:51 +0100 |
wenzelm |
bash process with builtin timing;
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 22:37:31 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 21:00:38 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2016 00:27:57 +0100 |
wenzelm |
proper return code for timeout (amending f868f12f9419);
|
file |
diff |
annotate
|
| Thu, 25 Feb 2016 00:18:48 +0100 |
wenzelm |
retain tail out_lines as printed, but not the whole log content;
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 23:36:45 +0100 |
wenzelm |
more informative Build.build_results;
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 22:40:19 +0100 |
wenzelm |
more informative Process_Result;
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 22:11:28 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|