diff -r 3e44f8c3f059 -r c46ff0efa1ce etc/settings
--- a/etc/settings	Wed May 19 11:48:35 2021 +0200
+++ b/etc/settings	Wed May 19 11:54:58 2021 +0200
@@ -72,7 +72,7 @@
 
 ISABELLE_LUALATEX="lualatex --interaction=nonstopmode --file-line-error"
 ISABELLE_BIBTEX="bibtex"
-ISABELLE_MAKEINDEX="makeindex"
+ISABELLE_MAKEINDEX="makeindex -c -q"
 ISABELLE_EPSTOPDF="epstopdf"