Wed, 09 Jun 2004 18:53:41 +0200 Sign.is_logtype;
wenzelm [Wed, 09 Jun 2004 18:53:41 +0200] rev 14901
Sign.is_logtype;
Wed, 09 Jun 2004 18:53:13 +0200 Syntax.default_mode;
wenzelm [Wed, 09 Jun 2004 18:53:13 +0200] rev 14900
Syntax.default_mode;
Wed, 09 Jun 2004 18:52:55 +0200 added option 'locale=NAME';
wenzelm [Wed, 09 Jun 2004 18:52:55 +0200] rev 14899
added option 'locale=NAME';
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip