Skip to content
Success

Changes

Summary

  1. tuned signature;
  2. clarified static Build_Process.Context vs. dynamic Build_Process.State; more dynamic Build_Process.Sessions, to accomodate multiple workers (and multiple builds);
  3. tuned signature: more operations;
  4. clarified signature: proper equals/hashCode;
  5. more robust database setup;
  6. clarified signature;
  7. clarified signature;
Changeset 78238:8c0d3c879f7c by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78237:c2c59de57df9 by wenzelm:
clarified static Build_Process.Context vs. dynamic Build_Process.State;<br>more dynamic Build_Process.Sessions, to accomodate multiple workers (and multiple builds);
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78236:f3a6140fa3b1 by wenzelm:
tuned signature: more operations;
The file was modified src/Pure/General/sha1.scala (diff)
Changeset 78235:aece9a063271 by wenzelm:
clarified signature: proper equals/hashCode;
The file was modified src/Pure/General/graph.scala (diff)
Changeset 78234:13863eaf372a by wenzelm:
more robust database setup;
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78233:1a12e6246212 by wenzelm:
clarified signature;
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_process.scala (diff)
Changeset 78232:45c7b88d1609 by wenzelm:
clarified signature;
The file was modified src/Pure/Tools/build.scala (diff)