diff -r aa14f630d8ef -r 564012e31db1 lib/Tools/latex
--- 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