Thu, 07 Jul 2011 23:55:15 +0200 | wenzelm | simplified make_option/dest_option; | changeset | files |
Thu, 07 Jul 2011 22:04:30 +0200 | wenzelm | explicit Document.Node.Header, with master_dir and thy_name; | changeset | files |
Thu, 07 Jul 2011 14:10:50 +0200 | wenzelm | explicit indication of type Symbol.Symbol; | changeset | files |