changeset 73740 | c46ff0efa1ce |
parent 48985 | 5386df44a037 |
--- a/src/Doc/sedindex Wed May 19 11:48:35 2021 +0200 +++ b/src/Doc/sedindex Wed May 19 11:54:58 2021 +0200 @@ -18,4 +18,4 @@ s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g s~\*\(\".\".\)~\1@{\\\\tt \1}~g s~\*\(\".\)~\1@{\\\\tt \1}~g -s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | makeindex -c -q -o $1.ind +s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | $ISABELLE_MAKEINDEX -o $1.ind