etc/settings
changeset 7864 5cd5a27f5c93
parent 7813 4412debd3004
child 7873 5d1200c7a671
equal deleted inserted replaced
7863:8b0aca9bdc26 7864:5cd5a27f5c93
    58 TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
    58 TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS"
    59 ISABELLE_LATEX="latex"
    59 ISABELLE_LATEX="latex"
    60 ISABELLE_PDFLATEX="pdflatex"
    60 ISABELLE_PDFLATEX="pdflatex"
    61 ISABELLE_BIBTEX="bibtex"
    61 ISABELLE_BIBTEX="bibtex"
    62 ISABELLE_DVIPS="dvips -D 600"
    62 ISABELLE_DVIPS="dvips -D 600"
       
    63 
       
    64 # The thumpdf tool is probably not generally available ...
       
    65 #ISABELLE_THUMBPDF="thumbpdf"
    63 
    66 
    64 
    67 
    65 ###
    68 ###
    66 ### Misc path settings
    69 ### Misc path settings
    67 ###
    70 ###