diff -r 9745b7d4cc79 -r bec95e287d26 Admin/lib/Tools/build_doc
--- a/Admin/lib/Tools/build_doc	Mon Aug 26 16:13:20 2013 +0200
+++ b/Admin/lib/Tools/build_doc	Mon Aug 26 16:51:53 2013 +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 "    -s           system build mode"
   echo
   echo "  Build Isabelle documentation from (doc) sessions."
   echo
@@ -37,12 +38,14 @@
 
 ## process command line
 
+declare -a BUILD_ARGS=()
+
+
 # options
 
 ALL_DOCS="false"
-JOBS=""
 
-while getopts "aj:" OPT
+while getopts "aj:s" OPT
 do
   case "$OPT" in
     a)
@@ -50,7 +53,11 @@
       ;;
     j)
       check_number "$OPTARG"
-      JOBS="-j $OPTARG"
+      BUILD_ARGS["${#BUILD_ARGS[@]}"]="-j"
+      BUILD_ARGS["${#BUILD_ARGS[@]}"]="$OPTARG"
+      ;;
+    s)
+      BUILD_ARGS["${#BUILD_ARGS[@]}"]="-s"
       ;;
     \?)
       usage
@@ -64,9 +71,9 @@
 # arguments
 
 if [ "$ALL_DOCS" = true ]; then
-  declare -a BUILD_ARGS=(-g doc)
+  BUILD_ARGS["${#BUILD_ARGS[@]}"]="-g"
+  BUILD_ARGS["${#BUILD_ARGS[@]}"]="doc"
 else
-  declare -a BUILD_ARGS=()
   [ "$#" -eq 0 ] && usage
 fi
 
@@ -83,12 +90,12 @@
 OUTPUT="$ISABELLE_TMP_PREFIX$$"
 mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""
 
-"$ISABELLE_TOOL" build -R -b $JOBS "${BUILD_ARGS[@]}"
+"$ISABELLE_TOOL" build -R -b "${BUILD_ARGS[@]}"
 RC=$?
 
 if [ "$RC" = 0 ]; then
   "$ISABELLE_TOOL" build -o browser_info=false -o "document=pdf" \
-    -o "document_output=$OUTPUT" -c $JOBS "${BUILD_ARGS[@]}"
+    -o "document_output=$OUTPUT" -c "${BUILD_ARGS[@]}"
   RC=$?
 fi