Summary
- clarified use of memory: prefer share tree structures over fresh strings;
- more Java heap space (see 2d658beb815b);
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | src/Pure/Admin/isabelle_cronjob.scala (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | src/Pure/Admin/isabelle_cronjob.scala (diff) |