Summary
- merged
- recovered document from 9bfb6978eb80;
- NEWS;
- obsolete;
- tuned;
- ROOT cleanup: empty 'document_files' means there is no document;
- eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
- more informative timeout message, notably for build_status;
- clarified: adapted to ML version;
- proper order of initialization (amending 9953ae603a23);
The file was modified | src/HOL/ROOT (diff) |
The file was modified | NEWS (diff) |
The file was modified | lib/Tools/mkroot (diff) |
The file was modified | src/Doc/System/Environment.thy (diff) |
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) |
The file was modified | src/Pure/Thy/present.ML (diff) |
The file was modified | src/Pure/Admin/build_log.scala (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | src/Pure/PIDE/markup.scala (diff) |