# HG changeset patch
# User wenzelm
# Date 1346664629 -7200
# Node ID 88fe93ae61cf202489a5be53ccf83c7fce3d1907
# Parent  747835eb2782a9bbc44f4294c82091b396514651
tuned boundary cases of command-line;
adhoc removal of PDFs stemming from base sessions;

diff -r 747835eb2782 -r 88fe93ae61cf Admin/lib/Tools/build_doc
--- a/Admin/lib/Tools/build_doc	Mon Sep 03 11:09:25 2012 +0200
+++ b/Admin/lib/Tools/build_doc	Mon Sep 03 11:30:29 2012 +0200
@@ -67,6 +67,7 @@
   declare -a BUILD_OPTIONS=(-g doc)
 else
   declare -a BUILD_OPTIONS=()
+  [ "$#" -eq 0 ] && usage
 fi
 
 
@@ -97,7 +98,12 @@
   do
     cp -f "$FILE" "$ISABELLE_HOME/doc"
   done
-  cp -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
+  if [ "$PDF_ONLY" = true ]; then
+    cp -f "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
+    rm -f "$ISABELLE_HOME/doc/document.pdf" "$ISABELLE_HOME/doc/outline.pdf"
+  else
+    cp -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
+  fi
 fi
 
 rm -rf "$OUTPUT"