Summary
- renamed lemmas
- build manager: echo error messages to server output;
- omit showing previous failures for user builds;
- always handle interrupted jobs;
- add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
- clarified context: operations now in build process;
- clarified: add explicit build process;
- remove unnecessary subdir;
- tuned;
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Library/FSet.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | src/HOL/Wellfounded.thy (diff) |
The file was modified | src/Pure/Build/build_manager.scala (diff) |
The file was modified | src/Pure/Build/build_manager.scala (diff) |
The file was modified | src/Pure/Build/build_manager.scala (diff) |
The file was modified | etc/options (diff) |
The file was modified | src/Pure/Admin/ci_build.scala (diff) |
The file was modified | src/Pure/Build/build_manager.scala (diff) |
The file was modified | src/Pure/Build/build_manager.scala (diff) |
The file was modified | src/Pure/Build/build_manager.scala (diff) |
The file was modified | src/Pure/Build/build_manager.scala (diff) |
The file was modified | src/Pure/Build/build_manager.scala (diff) |