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;