| Tue, 14 Oct 2008 15:45:46 +0200 | wenzelm | adding preferences is now permissive; | changeset | files |
| Tue, 14 Oct 2008 15:45:45 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 14 Oct 2008 15:45:44 +0200 | wenzelm | adding preferences is now permissive, no error handling here; | changeset | files |