equal
deleted
inserted
replaced
142 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
142 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
143 |
143 |
144 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \ |
144 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \ |
145 "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \ |
145 "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \ |
146 "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ |
146 "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ |
147 "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \ |
147 "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \ |
148 "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" |
148 "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" |
149 RC="$?" |
149 RC="$?" |
150 |
150 |
151 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then |
151 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then |
152 echo -n "Finished at "; date |
152 echo -n "Finished at "; date |