Summary
- more Java heap, e.g. relevant for hg.graph on Isabelle repository;
- more robust check -- do not rely on return code;
- more compact ML_Statistics, to make build_status work with less than 2GB heap;
- retain latest ml_stats (amending e76c6cb0d461);
The file was modified | etc/settings (diff) |
The file was modified | Admin/lib/Tools/makedist_bundle (diff) |
The file was modified | src/Pure/Admin/build_status.scala (diff) |
The file was modified | src/Pure/ML/ml_statistics.scala (diff) |
The file was modified | src/Pure/Admin/build_status.scala (diff) |