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