Thu, 12 Jul 2007 11:43:17 +0200 | wenzelm | updated; | changeset | files |
Thu, 12 Jul 2007 00:15:42 +0200 | wenzelm | tuned signature; | changeset | files |
Thu, 12 Jul 2007 00:15:41 +0200 | wenzelm | sys_error; | changeset | files |
Thu, 12 Jul 2007 00:15:39 +0200 | wenzelm | simplified using Markup.get_int; | changeset | files |