lib/Tools/fixdots
Thu, 09 Oct 1997 18:01:27 +0200 wenzelm \n at end;
Thu, 09 Oct 1997 17:45:03 +0200 wenzelm ensure that dots in formulas are followed by non-idents;
less more (0) tip