src/Pure/Build/build_cluster.scala
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");
less more (0) -10 -3 tip