diff -r 6bc647f472b9 -r 0f0a2148a099 etc/settings
--- a/etc/settings	Wed Jan 07 07:52:12 2004 +0100
+++ b/etc/settings	Thu Jan 08 04:32:52 2004 +0100
@@ -85,6 +85,9 @@
 # bibtex command for isatool latex/document
 ISABELLE_BIBTEX="bibtex"
 
+# makeindex command for isatool latex/document
+ISABELLE_MAKEINDEX="makeindex"
+
 # dvips command for isatool latex/document
 ISABELLE_DVIPS="dvips -D 600"