src/Pure/Build/build_manager.scala
Wed, 09 Apr 2025 22:23:59 +0200 wenzelm tuned: prefer explicit Bash.exports;
Thu, 27 Mar 2025 10:45:33 +0100 Fabian Huch start jobs even if repository is unreachable, e.g. due to high load;
Sun, 02 Feb 2025 00:11:06 +0100 Fabian Huch clarified name;
Sat, 01 Feb 2025 22:41:43 +0100 Fabian Huch tuned;
Sat, 01 Feb 2025 22:39:44 +0100 Fabian Huch use ssh host for default address;
Sat, 01 Feb 2025 22:30:09 +0100 Fabian Huch clarified option name;
Sat, 01 Feb 2025 22:28:32 +0100 Fabian Huch clarified options: extra ssh connection to cluster of build_manager;
Sat, 01 Feb 2025 22:20:42 +0100 Fabian Huch tuned output;
Sat, 01 Feb 2025 20:46:01 +0100 Fabian Huch tuned: more standard;
Mon, 20 Jan 2025 09:17:37 +0100 Fabian Huch clarified;
Fri, 17 Jan 2025 13:43:16 +0100 Fabian Huch tuned whitespace;
Tue, 27 Aug 2024 13:53:18 +0200 Fabian Huch stop web server on close;
Tue, 27 Aug 2024 13:44:23 +0200 Fabian Huch better results for terminated jobs;
Tue, 27 Aug 2024 13:12:10 +0200 Fabian Huch more robust: clean up unfinished jobs on init, e.g. if build_manager process was forcefully terminated;
Tue, 27 Aug 2024 12:57:49 +0200 Fabian Huch manage runner state properly (amending be4c1fbccfe8);
Wed, 21 Aug 2024 13:33:19 +0200 Fabian Huch remove terminated jobs, even if futures do not complete;
Tue, 20 Aug 2024 17:28:51 +0200 Fabian Huch terminate jobs properly;
Tue, 06 Aug 2024 18:39:32 +0200 Fabian Huch build_manager: change colors;
Tue, 06 Aug 2024 16:58:23 +0200 Fabian Huch build_manager: display more info;
Tue, 06 Aug 2024 15:40:51 +0200 Fabian Huch tuned and clarified;
Tue, 06 Aug 2024 15:38:10 +0200 Fabian Huch build_manager: store submitting user;
Tue, 06 Aug 2024 15:00:37 +0200 Fabian Huch build_manager: terminate processes if cancelling does not work;
Tue, 06 Aug 2024 13:54:10 +0200 Fabian Huch build_manager: log message when job is cancelled;
Thu, 18 Jul 2024 13:52:51 +0200 Fabian Huch better poller: don't start job when same version is already running;
Thu, 18 Jul 2024 13:08:11 +0200 Fabian Huch clarified: more uniform;
Wed, 10 Jul 2024 17:42:48 +0200 Fabian Huch tuned website;
Wed, 10 Jul 2024 17:31:17 +0200 Fabian Huch proper parse (amending dd86d35375a7);
Wed, 10 Jul 2024 17:04:44 +0200 Fabian Huch allow updating reports via build_manager_database tool, e.g. to generate hg logs/diffs;
Wed, 10 Jul 2024 17:01:51 +0200 Fabian Huch clarified;
Wed, 10 Jul 2024 16:58:39 +0200 Fabian Huch clarified;
less more (0) -100 -50 -30 tip