Summary
- merged
- more links;
- clarified priority: zero can mean unknown/long or irrelevant/short time;
- absent timing information means zero, according to 0070053570c4, f235646b1b73;
The file was modified | src/Tools/VSCode/README.md (diff) |
The file was modified | src/Pure/Isar/toplevel.ML (diff) |
The file was modified | src/Pure/Isar/toplevel.ML (diff) |
The file was modified | src/Pure/PIDE/resources.ML (diff) |
The file was modified | src/Pure/Thy/thy_info.ML (diff) |
The file was modified | src/Pure/Tools/build.ML (diff) |