| Tue, 14 May 2013 19:48:31 +0200 | wenzelm | more uniform Markup.parse_real; | changeset | files |
| Tue, 14 May 2013 19:30:21 +0200 | wenzelm | tuned signature; | changeset | files |
| Tue, 14 May 2013 16:54:47 +0200 | wenzelm | more robust load_timings: ignore JVM errors such as java.lang.OutOfMemoryError; | changeset | files |