Mon, 10 Jan 2011 16:45:28 +0100 | wenzelm | added merge_options convenience; | changeset | files |
Mon, 10 Jan 2011 16:07:16 +0100 | wenzelm | tuned string_of_int to avoid allocation for small integers; | changeset | files |
Mon, 10 Jan 2011 15:45:46 +0100 | wenzelm | eliminated Int.toString; | changeset | files |