--- a/lib/Tools/latex Sat Sep 26 11:43:25 2020 +0200
+++ b/lib/Tools/latex Sat Sep 26 14:29:46 2020 +0200
@@ -13,7 +13,7 @@
echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
echo
echo " Options are:"
- echo " -o FORMAT specify output format: pdf (default), dvi, bbl, idx, sty"
+ echo " -o FORMAT specify output format: pdf (default), bbl, idx, sty"
echo
echo " Run LaTeX (and related tools) on FILE (default root.tex),"
echo " producing the specified output format."
@@ -70,7 +70,6 @@
# operations
-function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_bibtex () {
$ISABELLE_BIBTEX </dev/null "$FILEBASE"
@@ -96,11 +95,6 @@
run_pdflatex
RC="$?"
;;
- dvi)
- check_root && \
- run_latex
- RC="$?"
- ;;
bbl)
check_root && \
run_bibtex