lib/Tools/build
changeset 48509 4854ced3e9d7
parent 48474 5b9d79c6323b
child 48511 37999ee01156
     1.1 --- a/lib/Tools/build	Thu Jul 26 11:52:08 2012 +0200
     1.2 +++ b/lib/Tools/build	Thu Jul 26 12:27:47 2012 +0200
     1.3 @@ -28,7 +28,8 @@
     1.4    echo "  Options are:"
     1.5    echo "    -a           all sessions"
     1.6    echo "    -b           build target images"
     1.7 -  echo "    -d DIR       additional session directory with ROOT file"
     1.8 +  echo "    -d DIR       include session directory with ROOT file"
     1.9 +  echo "    -g NAME      include session group NAME"
    1.10    echo "    -j INT       maximum number of jobs (default 1)"
    1.11    echo "    -n           no build -- test dependencies only"
    1.12    echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
    1.13 @@ -58,16 +59,16 @@
    1.14  
    1.15  ALL_SESSIONS=false
    1.16  BUILD_IMAGES=false
    1.17 +declare -a MORE_DIRS=()
    1.18 +declare -a SESSION_GROUPS=()
    1.19  MAX_JOBS=1
    1.20  NO_BUILD=false
    1.21 +eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    1.22  SYSTEM_MODE=false
    1.23  TIMING=false
    1.24  VERBOSE=false
    1.25  
    1.26 -declare -a MORE_DIRS=()
    1.27 -eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    1.28 -
    1.29 -while getopts "abd:j:no:stv" OPT
    1.30 +while getopts "abd:g:j:no:stv" OPT
    1.31  do
    1.32    case "$OPT" in
    1.33      a)
    1.34 @@ -79,6 +80,9 @@
    1.35      d)
    1.36        MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
    1.37        ;;
    1.38 +    g)
    1.39 +      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
    1.40 +      ;;
    1.41      j)
    1.42        check_number "$OPTARG"
    1.43        MAX_JOBS="$OPTARG"
    1.44 @@ -122,8 +126,8 @@
    1.45  fi
    1.46  
    1.47  "$ISABELLE_TOOL" java isabelle.Build \
    1.48 -  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" \
    1.49 -  "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    1.50 +  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \
    1.51 +  "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    1.52  RC="$?"
    1.53  
    1.54  if [ "$NO_BUILD" = false ]; then