lib/scripts/fixdots.pl
changeset 14981 e73f8140af78
parent 9789 7e5e6c47c0b5
equal deleted inserted replaced
14980:267cc670317a 14981:e73f8140af78
     1 #
     1 #
     2 # $Id$
     2 # $Id$
     3 # Author: Markus Wenzel, TU Muenchen
     3 # Author: Markus Wenzel, TU Muenchen
     4 # License: GPL (GNU GENERAL PUBLIC LICENSE)
       
     5 #
     4 #
     6 # fixdots.pl - ensure that dots in formulas are followed by non-idents
     5 # fixdots.pl - ensure that dots in formulas are followed by non-idents
     7 #
     6 #
     8 # tries to be smart; may produce garbage if nested comments and
     7 # tries to be smart; may produce garbage if nested comments and
     9 # solitary quotes (") are intermixed badly;
     8 # solitary quotes (") are intermixed badly;