# HG changeset patch
# User wenzelm
# Date 1396734981 -7200
# Node ID 96b54a96b1177b14db9c9a26301ffd590704d6d6
# Parent  4eb88149c7b2beaeeb78041dd30a04ff0293ba89
tuned;

diff -r 4eb88149c7b2 -r 96b54a96b117 Admin/lib/Tools/build_doc
--- a/Admin/lib/Tools/build_doc	Sat Apr 05 23:42:30 2014 +0200
+++ b/Admin/lib/Tools/build_doc	Sat Apr 05 23:56:21 2014 +0200
@@ -15,12 +15,12 @@
   echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]"
   echo
   echo "  Options are:"
-  echo "    -a           select all doc sessions"
+  echo "    -a           select all documentation sessions"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
   echo "    -s           system build mode"
   echo
-  echo "  Build Isabelle documentation from doc sessions with suitable"
-  echo "  document_variants."
+  echo "  Build Isabelle documentation from documentation sessions with"
+  echo "  suitable document_variants entry."
   echo
   exit 1
 }
diff -r 4eb88149c7b2 -r 96b54a96b117 src/Pure/Tools/build_doc.scala
--- a/src/Pure/Tools/build_doc.scala	Sat Apr 05 23:42:30 2014 +0200
+++ b/src/Pure/Tools/build_doc.scala	Sat Apr 05 23:56:21 2014 +0200
@@ -35,11 +35,11 @@
 
     docs.filter(doc => !selected_docs.contains(doc)) match {
       case Nil =>
-      case bad => error("No doc session for " + commas_quote(bad))
+      case bad => error("No documentation session for " + commas_quote(bad))
     }
 
+    progress.echo("Build started for documentation " + commas_quote(selected_docs))
 
-    progress.echo("Build started for documentation " + commas_quote(selected_docs))
     val rc1 =
       Build.build(options, progress, requirements = true, build_heap = true,
         max_jobs = max_jobs, system_mode = system_mode, sessions = sessions)