Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. recovered document from 9bfb6978eb80;
  3. NEWS;
  4. obsolete;
  5. tuned;
  6. ROOT cleanup: empty 'document_files' means there is no document;
  7. eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
  8. more informative timeout message, notably for build_status;
  9. clarified: adapted to ML version;
  10. proper order of initialization (amending 9953ae603a23);
Changeset 66951:dd4710b91277 by wenzelm:
merged
Changeset 66950:1a5e90026391 by wenzelm:
recovered document from 9bfb6978eb80;
The file was modified src/HOL/ROOT (diff)
Changeset 66949:6c5e4ac0398b by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 66948:47249c5ec3a4 by wenzelm:
obsolete;
The file was modified lib/Tools/mkroot (diff)
Changeset 66947:eefbb2300669 by wenzelm:
tuned;
The file was modified src/Doc/System/Environment.thy (diff)
Changeset 66946:3d8fd98c7c86 by wenzelm:
ROOT cleanup: empty 'document_files' means there is no document;
The file was modified src/Benchmarks/ROOT (diff)
The file was modified src/CCL/ROOT (diff)
The file was modified src/Cube/ROOT (diff)
The file was modified src/Doc/ROOT (diff)
The file was modified src/FOLP/ROOT (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/LCF/ROOT (diff)
The file was modified src/Sequents/ROOT (diff)
The file was modified src/ZF/ROOT (diff)
Changeset 66945:b6f787a17fbe by wenzelm:
eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
The file was modified src/Pure/Thy/present.ML (diff)
Changeset 66944:05df740cb54b by wenzelm:
more informative timeout message, notably for build_status;
The file was modified src/Pure/Admin/build_log.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 66943:351aaaa9bacd by wenzelm:
clarified: adapted to ML version;
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 66942:91a21a5631ae by wenzelm:
proper order of initialization (amending 9953ae603a23);
The file was modified src/Pure/PIDE/markup.scala (diff)