src/Doc/sedindex
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