| changeset 49002 | 8ce0fa01ea86 |
| parent 48988 | f4d4d6d6702b |
| child 49005 | 96d5e42e5e3a |
--- 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"