Summary
- misc updates;
- merged
- consolidate implicit use of gnutar, via somewhat fragile dynamic scoping within existing shell scripts;
- merged
- Liminf/Limsup and filtermap
- benchmark doesn't need to build documents
- benchmark profile runs on small worker now (6 cores)
- merged
- NEWS
- merged
- serious measurements require jobs = 1;
- sessions that are relevant for routine timing measurements;
- more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
The file was modified | Admin/Release/CHECKLIST (diff) |
The file was modified | Admin/Release/CHECKLIST (diff) |
The file was modified | Admin/Release/build_library (diff) |
The file was modified | Admin/java/build (diff) |
The file was modified | Admin/lib/Tools/makedist (diff) |
The file was modified | Admin/lib/Tools/makedist_bundle (diff) |
The file was modified | src/HOL/Library/Liminf_Limsup.thy (diff) |
The file was modified | Admin/jenkins/build/ci_build_benchmark.scala (diff) |
The file was modified | src/Pure/Tools/ci_profile.scala (diff) |
The file was modified | Admin/jenkins/build/ci_build_benchmark.scala (diff) |
The file was modified | NEWS (diff) |
The file was modified | Admin/jenkins/build/ci_build_benchmark.scala (diff) |
The file was modified | Admin/jenkins/build/ci_build_benchmark.scala (diff) |
The file was modified | src/HOL/ROOT (diff) |
The file was modified | src/ZF/ROOT (diff) |
The file was modified | src/Pure/General/completion.scala (diff) |