Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. build manager: manage directories/permissions, to minimize local administration;
Changeset 80253:a3c2868cfb5d by fabian huch _huch@in.tum.de_:
tuned;
The file was modified etc/options (diff)
Changeset 80252:96543177ab7e by fabian huch _huch@in.tum.de_:
build manager: manage directories/permissions, to minimize local administration;
The file was modified etc/options (diff)
The file was modified src/Pure/Build/build_manager.scala (diff)