Wed, 09 Jun 2004 18:54:26 +0200 removed separate logtypes field of syntax;
wenzelm [Wed, 09 Jun 2004 18:54:26 +0200] rev 14903
removed separate logtypes field of syntax;
Wed, 09 Jun 2004 18:54:07 +0200 Path.split_ext; more robust inform_file_processed;
wenzelm [Wed, 09 Jun 2004 18:54:07 +0200] rev 14902
Path.split_ext; more robust inform_file_processed;
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';
Wed, 09 Jun 2004 18:52:42 +0200 Url.File;
wenzelm [Wed, 09 Jun 2004 18:52:42 +0200] rev 14898
Url.File;
Wed, 09 Jun 2004 18:52:11 +0200 * Document preparation: antiquotations provide option 'locale=NAME';
wenzelm [Wed, 09 Jun 2004 18:52:11 +0200] rev 14897
* Document preparation: antiquotations provide option 'locale=NAME';
Wed, 09 Jun 2004 18:51:26 +0200 tuned comment;
wenzelm [Wed, 09 Jun 2004 18:51:26 +0200] rev 14896
tuned comment;
Wed, 09 Jun 2004 18:51:16 +0200 updated/tuned identifier syntax;
wenzelm [Wed, 09 Jun 2004 18:51:16 +0200] rev 14895
updated/tuned identifier syntax;
Wed, 09 Jun 2004 18:51:02 +0200 updated notes on sub-/superscripts;
wenzelm [Wed, 09 Jun 2004 18:51:02 +0200] rev 14894
updated notes on sub-/superscripts;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip