--- a/lib/Tools/document Sat Jul 27 22:16:04 2013 +0200
+++ b/lib/Tools/document Sat Jul 27 22:20:25 2013 +0200
@@ -15,7 +15,7 @@
echo " Options are:"
echo " -c cleanup -- be aggressive in removing old stuff"
echo " -n NAME specify document name (default 'document')"
- echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
+ echo " -o FORMAT specify output format: pdf (default), dvi"
echo " -t TAGS specify tagged region markup"
echo
echo " Prepare the theory session document in DIR (default 'document')"
@@ -37,7 +37,7 @@
CLEAN=""
NAME="document"
-OUTFORMAT=dvi
+OUTFORMAT=pdf
declare -a TAGS=()
while getopts "cn:o:t:" OPT
@@ -77,7 +77,7 @@
# check format
case "$OUTFORMAT" in
- dvi | dvi.gz | ps | ps.gz | pdf)
+ pdf | dvi)
;;
*)
fail "Bad output format '$OUTFORMAT'"