1.1 --- a/doc-src/fixbookmarks.pl Tue May 11 18:18:37 1999 +0200
1.2 +++ b/doc-src/fixbookmarks.pl Wed May 12 09:44:44 1999 +0200
1.3 @@ -1,4 +1,4 @@
1.4
1.5 -s/\\(\w+)\s*/$1/g;
1.6 +s/\\([a-zA-Z]+)\s*/$1/g;
1.7 s/\$//g;
1.8 s/^BOOKMARK/\\BOOKMARK/g;