# HG changeset patch
# User wenzelm
# Date 1346266489 -7200
# Node ID 8ce0fa01ea8687123c55727262cc896c129ddf1f
# Parent  c83370b55e468ae48ece16fbcb5972f2e4d6da77
one more round to ensure that base images are already there, without producing document output themselves;

diff -r c83370b55e46 -r 8ce0fa01ea86 Admin/lib/Tools/build_doc
--- a/Admin/lib/Tools/build_doc	Wed Aug 29 20:46:47 2012 +0200
+++ b/Admin/lib/Tools/build_doc	Wed Aug 29 20:54:49 2012 +0200
@@ -71,7 +71,7 @@
 mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""
 
 RC=0
-for FORMAT in dvi pdf
+for FORMAT in false dvi pdf
 do
   if [ "$RC" = 0 ]; then
     echo "Document format: $FORMAT"