Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned;
  3. clarified signature;
  4. minor performance tuning: avoid redundant server access;
  5. tuned;
  6. clarified modules and options (from store);
  7. clarified signature;
  8. tuned;
  9. clarified signature;
  10. tuned signature;
  11. tuned;
  12. tuned signature;
  13. tuned;
  14. tuned;
  15. more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
  16. tuned messages;
  17. tuned;
  18. back to static numa_nodes (reverting part of c2c59de57df9);
  19. tuned messages;
  20. canonical time function for List.nth
Changeset 80126:b73df63e0f52 by wenzelm:
merged
Changeset 80125:761bd2b35217 by wenzelm:
tuned;
The file was modified src/Pure/Build/build_benchmark.scala (diff)
The file was modified src/Pure/Build/build_schedule.scala (diff)
Changeset 80124:455ddb251ece by wenzelm:
clarified signature;
The file was modified src/Pure/Build/build_benchmark.scala (diff)
The file was modified src/Pure/Build/build_process.scala (diff)
The file was modified src/Pure/Build/build_schedule.scala (diff)
The file was modified src/Pure/ML/ml_process.scala (diff)
Changeset 80123:7e4c3bb3d062 by wenzelm:
minor performance tuning: avoid redundant server access;
The file was modified src/Pure/Build/store.scala (diff)
Changeset 80122:66d7a923b750 by wenzelm:
tuned;
The file was modified src/Pure/Build/store.scala (diff)
Changeset 80121:05cec0a3c63d by wenzelm:
clarified modules and options (from store);
The file was modified src/Pure/Build/build_job.scala (diff)
The file was modified src/Pure/Build/store.scala (diff)
Changeset 80120:370ebda8bd86 by wenzelm:
clarified signature;
The file was modified src/Pure/Build/build_job.scala (diff)
The file was modified src/Pure/Build/store.scala (diff)
Changeset 80119:47f671888a37 by wenzelm:
tuned;
The file was modified src/Pure/Tools/update.scala (diff)
Changeset 80118:0323cd9fcab9 by wenzelm:
clarified signature;
The file was modified src/Pure/Build/build.scala (diff)
The file was modified src/Pure/Build/build_process.scala (diff)
The file was modified src/Pure/Build/build_schedule.scala (diff)
Changeset 80117:61b8f6ac6860 by wenzelm:
tuned signature;
The file was modified src/Pure/Build/build_benchmark.scala (diff)
The file was modified src/Pure/Build/store.scala (diff)
Changeset 80116:d510a1cf9965 by wenzelm:
tuned;
The file was modified src/Pure/Build/build.scala (diff)
Changeset 80115:d4d9a7887b2a by wenzelm:
tuned signature;
The file was modified src/Pure/Build/build_job.scala (diff)
Changeset 80114:c188068e41f1 by wenzelm:
tuned;
The file was modified src/Pure/ML/ml_heap.scala (diff)
Changeset 80113:4b95a1d8b2c9 by wenzelm:
tuned;
The file was modified src/Pure/ML/ml_heap.scala (diff)
Changeset 80112:c729b1d58982 by wenzelm:
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
The file was modified src/Pure/ML/ml_heap.scala (diff)
Changeset 80111:f4d3e3915228 by wenzelm:
tuned messages;
The file was modified src/Pure/Build/store.scala (diff)
Changeset 80110:2ac132ee8bf1 by wenzelm:
tuned;
The file was modified src/Pure/Build/build_process.scala (diff)
Changeset 80109:dbcd6dc7f70f by wenzelm:
back to static numa_nodes (reverting part of c2c59de57df9);
The file was modified src/Pure/Build/build.scala (diff)
The file was modified src/Pure/Build/build_process.scala (diff)
The file was modified src/Pure/Build/build_schedule.scala (diff)
Changeset 80108:6ec65767d7bd by wenzelm:
tuned messages;
The file was modified src/Pure/ML/ml_heap.scala (diff)
Changeset 80107:247751d25102 by manuel eberl _eberlm@in.tum.de_:
canonical time function for List.nth
The file was modified src/HOL/Data_Structures/Selection.thy (diff)
The file was modified src/HOL/Data_Structures/Time_Funs.thy (diff)