equal
deleted
inserted
replaced
25 echo |
25 echo |
26 echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]" |
26 echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]" |
27 echo |
27 echo |
28 echo " Options are:" |
28 echo " Options are:" |
29 echo " -a all sessions" |
29 echo " -a all sessions" |
30 echo " -b build target images" |
30 echo " -b build heap images" |
31 echo " -d DIR include session directory with ROOT file" |
31 echo " -d DIR include session directory with ROOT file" |
32 echo " -g NAME include session group NAME" |
32 echo " -g NAME include session group NAME" |
33 echo " -j INT maximum number of jobs (default 1)" |
33 echo " -j INT maximum number of jobs (default 1)" |
34 echo " -n no build -- test dependencies only" |
34 echo " -n no build -- test dependencies only" |
35 echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" |
35 echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" |
56 |
56 |
57 |
57 |
58 ## process command line |
58 ## process command line |
59 |
59 |
60 ALL_SESSIONS=false |
60 ALL_SESSIONS=false |
61 BUILD_IMAGES=false |
61 BUILD_HEAP=false |
62 declare -a MORE_DIRS=() |
62 declare -a MORE_DIRS=() |
63 declare -a SESSION_GROUPS=() |
63 declare -a SESSION_GROUPS=() |
64 MAX_JOBS=1 |
64 MAX_JOBS=1 |
65 NO_BUILD=false |
65 NO_BUILD=false |
66 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" |
66 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" |
73 case "$OPT" in |
73 case "$OPT" in |
74 a) |
74 a) |
75 ALL_SESSIONS="true" |
75 ALL_SESSIONS="true" |
76 ;; |
76 ;; |
77 b) |
77 b) |
78 BUILD_IMAGES="true" |
78 BUILD_HEAP="true" |
79 ;; |
79 ;; |
80 d) |
80 d) |
81 MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG" |
81 MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG" |
82 ;; |
82 ;; |
83 g) |
83 g) |
124 fi |
124 fi |
125 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
125 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
126 fi |
126 fi |
127 |
127 |
128 "$ISABELLE_TOOL" java isabelle.Build \ |
128 "$ISABELLE_TOOL" java isabelle.Build \ |
129 "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \ |
129 "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \ |
130 "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" |
130 "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" |
131 RC="$?" |
131 RC="$?" |
132 |
132 |
133 if [ "$NO_BUILD" = false ]; then |
133 if [ "$NO_BUILD" = false ]; then |
134 echo -n "Finished at "; date |
134 echo -n "Finished at "; date |