etc/settings
changeset 14344 0f0a2148a099
parent 14253 91a64a93bdb4
child 14447 5b61dc4eab24
equal deleted inserted replaced
14343:6bc647f472b9 14344:0f0a2148a099
    83 ISABELLE_PDFLATEX="pdflatex"
    83 ISABELLE_PDFLATEX="pdflatex"
    84 
    84 
    85 # bibtex command for isatool latex/document
    85 # bibtex command for isatool latex/document
    86 ISABELLE_BIBTEX="bibtex"
    86 ISABELLE_BIBTEX="bibtex"
    87 
    87 
       
    88 # makeindex command for isatool latex/document
       
    89 ISABELLE_MAKEINDEX="makeindex"
       
    90 
    88 # dvips command for isatool latex/document
    91 # dvips command for isatool latex/document
    89 ISABELLE_DVIPS="dvips -D 600"
    92 ISABELLE_DVIPS="dvips -D 600"
    90 
    93 
    91 # epstopdf command for isatool latex/document
    94 # epstopdf command for isatool latex/document
    92 ISABELLE_EPSTOPDF="epstopdf"
    95 ISABELLE_EPSTOPDF="epstopdf"