1.1 --- a/doc-src/TutorialI/isa-index	Wed Jul 11 13:55:15 2001 +0200
     1.2 +++ b/doc-src/TutorialI/isa-index	Wed Jul 11 13:55:43 2001 +0200
     1.3 @@ -16,8 +16,8 @@
     1.4  # change *IDENT  to  IDENT@{\tt IDENT}  
     1.5  #    where IDENT is any string not containing | ! or @
     1.6  # FOUR backslashes: to escape the shell AND sed
     1.7 -sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\isa{\1}}~g
     1.8 -s~\*\(\".\".\".\)~\1@{\\\\isa{\1}}~g
     1.9 -s~\*\(\".\".\)~\1@{\\\\isa{\1}}~g
    1.10 -s~\*\(\".\)~\1@{\\\\isa{\1}}~g
    1.11 -s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\isa{\1}}~g" $1.idx | makeindex -c -q -o $1.ind
    1.12 +sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
    1.13 +s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
    1.14 +s~\*\(\".\".\)~\1@\\\\isa {\1}~g
    1.15 +s~\*\(\".\)~\1@\\\\isa {\1}~g
    1.16 +s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind