| Fri, 03 Sep 2010 17:54:43 +0200 | wenzelm | disposed left-over user preferences; | changeset | files |
| Fri, 03 Sep 2010 17:43:44 +0200 | wenzelm | turned show_all_types into proper configuration option; | changeset | files |
| Fri, 03 Sep 2010 16:36:33 +0200 | wenzelm | treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter; | changeset | files |
| Fri, 03 Sep 2010 16:09:12 +0200 | wenzelm | more explicit Config.declare vs. Config.declare_global; | changeset | files |
| Fri, 03 Sep 2010 15:54:03 +0200 | wenzelm | turned show_no_free_types into proper configuration option show_free_types, with flipped polarity; | changeset | files |
| Fri, 03 Sep 2010 14:20:47 +0200 | blanchet | remove code I submitted accidentally | changeset | files |