etc/settings
changeset 7813 4412debd3004
parent 7776 8fd408765c1d
child 7864 5cd5a27f5c93
equal deleted inserted replaced
7812:a8a21d7a83a1 7813:4412debd3004
    56 ###
    56 ###
    57 
    57 
    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_DVIPS="dvips -D 600"
    62 ISABELLE_DVIPS="dvips -D 600"
    62 
    63 
    63 
    64 
    64 ###
    65 ###
    65 ### Misc path settings
    66 ### Misc path settings