Skip to content
Success

Changes

Summary

  1. tuned;
  2. tuned spelling;
  3. support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
  4. clarified signature;
  5. more general dirs for Sync.sync;
  6. tuned whitespace (amending beb4ee344c22);
  7. clarified signature (see also be0ab4b94c62 and c41791ad75c3);
Changeset 80200:5f053991315c by wenzelm:
tuned;
The file was modified src/Pure/Build/build_cluster.scala (diff)
Changeset 80199:987424bebeb9 by wenzelm:
tuned spelling;
The file was modified src/Pure/Build/build_cluster.scala (diff)
Changeset 80198:7883f221d6d3 by wenzelm:
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
The file was modified src/Pure/Build/build_cluster.scala (diff)
Changeset 80197:36547884db60 by wenzelm:
clarified signature;
The file was modified src/Pure/General/mercurial.scala (diff)
Changeset 80196:9308bc5f65d6 by wenzelm:
more general dirs for Sync.sync;
The file was modified src/Pure/Admin/build_history.scala (diff)
The file was modified src/Pure/Build/build.scala (diff)
The file was modified src/Pure/Build/build_cluster.scala (diff)
The file was modified src/Pure/Tools/sync.scala (diff)
Changeset 80195:e2ccabd7a857 by wenzelm:
tuned whitespace (amending beb4ee344c22);
The file was modified ROOTS (diff)
Changeset 80194:79655411a32d by wenzelm:
clarified signature (see also be0ab4b94c62 and c41791ad75c3);
The file was modified src/Pure/Build/sessions.scala (diff)
The file was modified src/Pure/General/file.scala (diff)