Wed, 09 Jun 2004 18:53:41 +0200 | wenzelm | Sign.is_logtype; | changeset | files |
Wed, 09 Jun 2004 18:53:13 +0200 | wenzelm | Syntax.default_mode; | changeset | files |
Wed, 09 Jun 2004 18:52:55 +0200 | wenzelm | added option 'locale=NAME'; | changeset | files |