equal
deleted
inserted
replaced
69 |
69 |
70 OUTPUT="$ISABELLE_TMP_PREFIX$$" |
70 OUTPUT="$ISABELLE_TMP_PREFIX$$" |
71 mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\"" |
71 mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\"" |
72 |
72 |
73 RC=0 |
73 RC=0 |
74 for FORMAT in dvi pdf |
74 for FORMAT in false dvi pdf |
75 do |
75 do |
76 if [ "$RC" = 0 ]; then |
76 if [ "$RC" = 0 ]; then |
77 echo "Document format: $FORMAT" |
77 echo "Document format: $FORMAT" |
78 "$ISABELLE_TOOL" build -o browser_info=false -o "document=$FORMAT" \ |
78 "$ISABELLE_TOOL" build -o browser_info=false -o "document=$FORMAT" \ |
79 -o "document_output=$OUTPUT" -c $JOBS "${BUILD_OPTIONS[@]}" -- "$@" |
79 -o "document_output=$OUTPUT" -c $JOBS "${BUILD_OPTIONS[@]}" -- "$@" |