Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. misc updates;
  2. merged
  3. consolidate implicit use of gnutar, via somewhat fragile dynamic scoping within existing shell scripts;
  4. merged
  5. Liminf/Limsup and filtermap
  6. benchmark doesn't need to build documents
  7. benchmark profile runs on small worker now (6 cores)
  8. merged
  9. NEWS
  10. merged
  11. serious measurements require jobs = 1;
  12. sessions that are relevant for routine timing measurements;
  13. more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
Changeset 63899:dc036b1a2a6f by wenzelm:
misc updates;
The file was modified Admin/Release/CHECKLIST (diff)
Changeset 63898:8a4b41a8afb8 by wenzelm:
merged
Changeset 63897:85c83757788c by wenzelm:
consolidate implicit use of gnutar, via somewhat fragile dynamic scoping within existing shell scripts;
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)
Changeset 63896:19979c2f0d4a by immler:
merged
Changeset 63895:9afa979137da by immler:
Liminf/Limsup and filtermap
The file was modified src/HOL/Library/Liminf_Limsup.thy (diff)
Changeset 63894:7534eec7cfad by lars hupel _lars.hupel@mytum.de_:
benchmark doesn't need to build documents
The file was modified Admin/jenkins/build/ci_build_benchmark.scala (diff)
The file was modified src/Pure/Tools/ci_profile.scala (diff)
Changeset 63893:c181a84eb6de by lars hupel _lars.hupel@mytum.de_:
benchmark profile runs on small worker now (6 cores)
The file was modified Admin/jenkins/build/ci_build_benchmark.scala (diff)
Changeset 63892:c17733350344 by traytel:
merged
Changeset 63891:8947157ca830 by traytel:
NEWS
The file was modified NEWS (diff)
Changeset 63890:3dd6bde2502d by wenzelm:
merged
Changeset 63889:2195a7e04db5 by wenzelm:
serious measurements require jobs = 1;
The file was modified Admin/jenkins/build/ci_build_benchmark.scala (diff)
Changeset 63888:5a9a1985e9fb by wenzelm:
sessions that are relevant for routine timing measurements;
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)
Changeset 63887:2d9c12eba726 by wenzelm:
more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
The file was modified src/Pure/General/completion.scala (diff)