Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. performance optimization;
  2. clarified names;
  3. clarified scheduler: proper split into scheduler, generator, and priority rules (following 32d00ec387f4);
  4. proper "linux_arm", amending 76ad72736e9e;
Changeset 79594:f933e9153624 by fabian huch _huch@in.tum.de_:
performance optimization;
The file was modified src/Pure/Build/build_schedule.scala (diff)
Changeset 79593:587a7dfeb03c by fabian huch _huch@in.tum.de_:
clarified names;
The file was modified src/Pure/Build/build_schedule.scala (diff)
Changeset 79592:7db599be70cc by fabian huch _huch@in.tum.de_:
clarified scheduler: proper split into scheduler, generator, and priority rules (following 32d00ec387f4);
The file was modified src/Pure/Build/build_schedule.scala (diff)
Changeset 79591:6e5f40cfa877 by wenzelm:
proper "linux_arm", amending 76ad72736e9e;
The file was modified Admin/components/PLATFORMS (diff)