1.1 --- a/doc-src/sedindex	Fri May 02 16:18:11 1997 +0200
     1.2 +++ b/doc-src/sedindex	Fri May 02 16:18:49 1997 +0200
     1.3 @@ -5,18 +5,17 @@
     1.4  #  puts strings prefixed by * into \tt font
     1.5  #    terminator characters for strings are |!@{}
     1.6  #
     1.7 -# uses \ptt instead of \tt since that happens to explicit \tt's 
     1.8  # a space terminates the \tt part to allow \index{*NE theorem}, etc.
     1.9  #
    1.10 -# change *"X"Y"Z"W  to  "X"Y"Z"W@{\ptt "X"Y"Z"W}
    1.11 -# change *"X"Y"Z    to  "X"Y"Z@{\ptt "X"Y"Z}
    1.12 -# change *"X"Y      to  "X"Y@{\ptt "X"Y}
    1.13 -# change *"X        to  "X@{\ptt "X}
    1.14 -# change *IDENT  to  IDENT@{\ptt IDENT}  
    1.15 +# change *"X"Y"Z"W  to  "X"Y"Z"W@{\tt "X"Y"Z"W}
    1.16 +# change *"X"Y"Z    to  "X"Y"Z@{\tt "X"Y"Z}
    1.17 +# change *"X"Y      to  "X"Y@{\tt "X"Y}
    1.18 +# change *"X        to  "X@{\tt "X}
    1.19 +# change *IDENT  to  IDENT@{\tt IDENT}  
    1.20  #    where IDENT is any string not containing | ! or @
    1.21  # FOUR backslashes: to escape the shell AND sed
    1.22 -sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\ptt \1}~g
    1.23 -s~\*\(\".\".\".\)~\1@{\\\\ptt \1}~g
    1.24 -s~\*\(\".\".\)~\1@{\\\\ptt \1}~g
    1.25 -s~\*\(\".\)~\1@{\\\\ptt \1}~g
    1.26 -s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\ptt \1}~g" $1.idx | makeindex -c -q -o $1.ind
    1.27 +sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\tt \1}~g
    1.28 +s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g
    1.29 +s~\*\(\".\".\)~\1@{\\\\tt \1}~g
    1.30 +s~\*\(\".\)~\1@{\\\\tt \1}~g
    1.31 +s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | makeindex -c -q -o $1.ind