tuned;
authorwenzelm
Wed May 12 09:44:44 1999 +0200 (1999-05-12)
changeset 663680052270f08b
parent 6635 f81b9b4c3265
child 6637 57abed64dc14
tuned;
doc-src/fixbookmarks.pl
     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;