src/Pure/Build/build_cluster.scala
Sun, 15 Jun 2025 23:09:43 +0200 wenzelm tuned message;
Sun, 15 Jun 2025 15:19:03 +0200 wenzelm clarified signature: more modular, avoid adhoc mixins;
Sat, 14 Jun 2025 21:19:37 +0200 wenzelm clarified signature;
Sat, 25 May 2024 20:26:06 +0200 wenzelm tuned;
Sat, 25 May 2024 20:10:17 +0200 wenzelm tuned spelling;
Sat, 25 May 2024 20:08:01 +0200 wenzelm support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
Sat, 25 May 2024 17:22:05 +0200 wenzelm more general dirs for Sync.sync;
less more (0) -10 -7 tip