| Wed, 01 Aug 2007 16:55:44 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 01 Aug 2007 16:55:43 +0200 | wenzelm | renamed 'print_options' to 'print_configs'; | changeset | files |
| Wed, 01 Aug 2007 16:55:42 +0200 | wenzelm | renamed config_option.ML to config.ML; | changeset | files |
| Wed, 01 Aug 2007 16:55:41 +0200 | wenzelm | renamed config_option.ML to config.ML; | changeset | files |
| Wed, 01 Aug 2007 16:55:40 +0200 | wenzelm | simplified internal Config interface; | changeset | files |
| Wed, 01 Aug 2007 16:55:39 +0200 | wenzelm | updated; | changeset | files |
| Wed, 01 Aug 2007 16:55:37 +0200 | wenzelm | tuned config options: eliminated separate attribute "option"; | changeset | files |