changeset 14344 | 0f0a2148a099 |
parent 14253 | 91a64a93bdb4 |
child 14447 | 5b61dc4eab24 |
--- 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"