| Fri, 03 Sep 2010 20:39:38 +0200 | wenzelm | tuned comment; | changeset | files |
| Fri, 03 Sep 2010 18:03:48 +0200 | wenzelm | merged | changeset | files |
| Fri, 03 Sep 2010 16:08:19 +0200 | haftmann | merged | changeset | files |
| Fri, 03 Sep 2010 16:08:09 +0200 | haftmann | QND_FLAG is a shell variable, not a string | changeset | files |
| Fri, 03 Sep 2010 17:57:12 +0200 | wenzelm | modernized session ROOT; | changeset | files |
| 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 |