tuned boundary cases of command-line;
adhoc removal of PDFs stemming from base sessions;

--- 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"