doc-src/fixbookmarks.pl
author haftmann
Fri Jan 22 13:38:28 2010 +0100 (2010-01-22)
changeset 34944 970e1466028d
parent 6636 80052270f08b
permissions -rw-r--r--
code literals: distinguish numeral classes by different entries
     1 
     2 s/\\([a-zA-Z]+)\s*/$1/g;
     3 s/\$//g;
     4 s/^BOOKMARK/\\BOOKMARK/g;