Admin/lib/Tools/build_doc
changeset 49005 96d5e42e5e3a
parent 49002 8ce0fa01ea86
child 49073 88fe93ae61cf
--- a/Admin/lib/Tools/build_doc	Wed Aug 29 21:20:46 2012 +0200
+++ b/Admin/lib/Tools/build_doc	Wed Aug 29 21:27:32 2012 +0200
@@ -17,6 +17,7 @@
   echo "  Options are:"
   echo "    -a           select all doc sessions"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
+  echo "    -p           approximative build of pdf documents"
   echo
   echo "  Build Isabelle documentation from (doc) sessions."
   echo
@@ -39,8 +40,9 @@
 
 ALL_DOCS="false"
 JOBS=""
+PDF_ONLY=""
 
-while getopts "aj:" OPT
+while getopts "aj:p" OPT
 do
   case "$OPT" in
     a)
@@ -50,6 +52,9 @@
       check_number "$OPTARG"
       JOBS="-j $OPTARG"
       ;;
+    p)
+      PDF_ONLY="true"
+      ;;
     \?)
       usage
       ;;
@@ -70,8 +75,14 @@
 OUTPUT="$ISABELLE_TMP_PREFIX$$"
 mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""
 
+if [ "$PDF_ONLY" = true ]; then
+  FORMATS="pdf"
+else
+  FORMATS="false dvi pdf"
+fi
+
 RC=0
-for FORMAT in false dvi pdf
+for FORMAT in $FORMATS
 do
   if [ "$RC" = 0 ]; then
     echo "Document format: $FORMAT"