src/Pure/System/process_result.scala
Wed, 08 Jul 2020 14:43:02 +0200 wenzelm more robust protocol for "Timing ..." messages, notably for pide_session=true;
Mon, 13 Apr 2020 17:40:44 +0200 wenzelm tuned message;
Mon, 13 Apr 2020 16:32:56 +0200 wenzelm tuned message;
Mon, 13 Apr 2020 16:16:22 +0200 wenzelm clarified signature;
Wed, 01 Apr 2020 18:19:46 +0200 wenzelm clarified signature: more robust;
Mon, 30 Mar 2020 19:39:11 +0200 wenzelm more accurate treatment of errors;
Fri, 07 Sep 2018 19:11:16 +0200 wenzelm tuned signature;
Sun, 06 May 2018 23:01:45 +0200 wenzelm tuned signature;
Wed, 26 Oct 2016 16:04:05 +0200 wenzelm clarified hg push return code: 1 means "nothing to push";
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;
Mon, 03 Oct 2016 20:09:50 +0200 wenzelm more operations;
Wed, 09 Mar 2016 14:54:51 +0100 wenzelm bash process with builtin timing;
Mon, 07 Mar 2016 22:37:31 +0100 wenzelm tuned signature;
Tue, 01 Mar 2016 21:00:38 +0100 wenzelm clarified modules;
Thu, 25 Feb 2016 00:27:57 +0100 wenzelm proper return code for timeout (amending f868f12f9419);
Thu, 25 Feb 2016 00:18:48 +0100 wenzelm retain tail out_lines as printed, but not the whole log content;
Wed, 24 Feb 2016 23:36:45 +0100 wenzelm more informative Build.build_results;
Wed, 24 Feb 2016 22:40:19 +0100 wenzelm more informative Process_Result;
Wed, 24 Feb 2016 22:11:28 +0100 wenzelm clarified modules;
less more (0) tip