1.1 --- a/doc-src/sedindex Tue May 03 18:12:54 1994 +0200
1.2 +++ b/doc-src/sedindex Tue May 03 18:27:30 1994 +0200
1.3 @@ -5,15 +5,18 @@
1.4 # puts strings prefixed by * into \tt font
1.5 # terminator characters for strings are |!@{}
1.6 #
1.7 -# change *"X"Y"Z"W to "X"Y"Z"W@{\tt "X"Y"Z"W}
1.8 -# change *"X"Y"Z to "X"Y"Z@{\tt "X"Y"Z}
1.9 -# change *"X"Y to "X"Y@{\tt "X"Y}
1.10 -# change *"X to "X@{\tt "X}
1.11 -# change *IDENT to IDENT@{\tt IDENT}
1.12 +# uses \ptt instead of \tt since that happens to explicit \tt's
1.13 +# a space terminates the \tt part to allow \index{*NE theorem}, etc.
1.14 +#
1.15 +# change *"X"Y"Z"W to "X"Y"Z"W@{\ptt "X"Y"Z"W}
1.16 +# change *"X"Y"Z to "X"Y"Z@{\ptt "X"Y"Z}
1.17 +# change *"X"Y to "X"Y@{\ptt "X"Y}
1.18 +# change *"X to "X@{\ptt "X}
1.19 +# change *IDENT to IDENT@{\ptt 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@{\\\\tt \1}~g
1.23 -s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g
1.24 -s~\*\(\".\".\)~\1@{\\\\tt \1}~g
1.25 -s~\*\(\".\)~\1@{\\\\tt \1}~g
1.26 -s~\*\([^|!@{}][^|!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | makeindex -q -o $1.ind
1.27 +sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\ptt \1}~g
1.28 +s~\*\(\".\".\".\)~\1@{\\\\ptt \1}~g
1.29 +s~\*\(\".\".\)~\1@{\\\\ptt \1}~g
1.30 +s~\*\(\".\)~\1@{\\\\ptt \1}~g
1.31 +s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\ptt \1}~g" $1.idx | makeindex -c -q -o $1.ind