equal
deleted
inserted
replaced
16 # FOUR backslashes: to escape the shell AND sed |
16 # FOUR backslashes: to escape the shell AND sed |
17 sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\tt \1}~g |
17 sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\tt \1}~g |
18 s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g |
18 s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g |
19 s~\*\(\".\".\)~\1@{\\\\tt \1}~g |
19 s~\*\(\".\".\)~\1@{\\\\tt \1}~g |
20 s~\*\(\".\)~\1@{\\\\tt \1}~g |
20 s~\*\(\".\)~\1@{\\\\tt \1}~g |
21 s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | makeindex -c -q -o $1.ind |
21 s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | $ISABELLE_MAKEINDEX -o $1.ind |