| Tue, 14 May 2013 16:54:47 +0200 | wenzelm | more robust load_timings: ignore JVM errors such as java.lang.OutOfMemoryError; | changeset | files |
| Tue, 14 May 2013 16:45:09 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 14 May 2013 16:04:26 +0200 | wenzelm | misc tuning and simplification; | changeset | files |
| Tue, 14 May 2013 15:40:18 +0200 | wenzelm | more frugal line termination, to cope with huge log files (see also 016cb7d8f297); | changeset | files |
| Tue, 14 May 2013 14:17:56 +0200 | wenzelm | more scalable File.write via separate chunks; | changeset | files |
| Tue, 14 May 2013 13:46:33 +0200 | wenzelm | more scalable Library.separate -- NB: JVM has tiny fixed-size stack; | changeset | files |