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