Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper check;
  2. proper symbolic hostname, as provided via Build_Cluster.Host;
  3. unused;
  4. clarified signature: Build_Cluster.Session.build_context; proper implementation of Build_Cluster.Session.start() based on Build.build_worker_command();
  5. clarified exception handling and return_code;
  6. tuned signature: more operations;
  7. more robust;
  8. support for Build_Cluster.Session.init (rsync + Admin/init); clarified Build.Results and overall return code;
  9. prefer Process_Result.RC.merge: strict treatment of interrupt;
  10. clarified signature: more operations;
  11. proper afp_root;
Changeset 78447:43cbd96de418 by wenzelm:
proper check;
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78446:9067d8ac9c47 by wenzelm:
proper symbolic hostname, as provided via Build_Cluster.Host;
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 78445:d70dc78c0d4e by wenzelm:
unused;
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78444:3d1746a716fa by wenzelm:
clarified signature: Build_Cluster.Session.build_context;<br>proper implementation of Build_Cluster.Session.start() based on Build.build_worker_command();
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78443:a8e1d9202dd9 by wenzelm:
clarified exception handling and return_code;
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78442:c38aebdf1a3d by wenzelm:
tuned signature: more operations;
The file was modified src/Pure/System/process_result.scala (diff)
Changeset 78441:3153311f0f6c by wenzelm:
more robust;
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78440:126a12483c67 by wenzelm:
support for Build_Cluster.Session.init (rsync + Admin/init);<br>clarified Build.Results and overall return code;
The file was modified etc/options (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_cluster.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78439:001d423daf7c by wenzelm:
prefer Process_Result.RC.merge: strict treatment of interrupt;
The file was modified src/HOL/Tools/Nitpick/kodkod.scala (diff)
The file was modified src/Pure/Admin/build_history.scala (diff)
Changeset 78438:d79eb2a6de0f by wenzelm:
clarified signature: more operations;
The file was modified src/Pure/System/process_result.scala (diff)
Changeset 78437:84471794b280 by wenzelm:
proper afp_root;
The file was modified src/Pure/Tools/build.scala (diff)