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"