lib/Tools/mkdir
Thu, 09 Nov 2000 21:38:00 +0100 wenzelm fixed \title: convert "_" to "-";
Mon, 30 Oct 2000 18:22:20 +0100 wenzelm tuned tex template;
Mon, 23 Oct 2000 22:09:52 +0200 wenzelm make sure default document works;
Mon, 18 Sep 2000 17:56:44 +0200 wenzelm best-style made default;
Fri, 01 Sep 2000 17:50:36 +0200 wenzelm GPLed;
Sat, 19 Aug 2000 12:42:52 +0200 wenzelm %\urlstyle{rm}
Tue, 04 Jul 2000 01:10:53 +0200 wenzelm fixed usage;
less more (0) -10 -7 tip