doc-src/fixbookmarks.pl
author huffman
Sat, 19 Dec 2009 09:07:04 -0800
changeset 34149 a0efb4754cb7
parent 6636 80052270f08b
permissions -rw-r--r--
add 'morphisms' option to domain_isomorphism command


s/\\([a-zA-Z]+)\s*/$1/g;
s/\$//g;
s/^BOOKMARK/\\BOOKMARK/g;