Summary
- avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);
- clarified "consolidation" vs. "presentation";
- tuned signature;
The file was modified | src/Pure/Tools/build.ML (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | etc/options (diff) |
The file was modified | src/Pure/PIDE/document.ML (diff) |
The file was modified | src/Pure/Concurrent/future.ML (diff) |