src/Pure/Build/build_manager.scala
Wed, 06 Aug 2025 16:51:58 +0200 Fabian Huch tuned doc: display build manager SSH options;
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;
less more (0) -100 -30 -10 -7 tip