back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc);
authorwenzelm
Wed Jul 15 11:25:51 2015 +0200 (2015-07-15)
changeset 607266d500a224cbe
parent 60725 daf200e2d79a
child 60727 53697011b03a
child 60729 f5989a2c1f67
back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc);
Admin/isatest/isatest-makeall
     1.1 --- a/Admin/isatest/isatest-makeall	Tue Jul 14 19:08:40 2015 +0200
     1.2 +++ b/Admin/isatest/isatest-makeall	Wed Jul 15 11:25:51 2015 +0200
     1.3 @@ -47,7 +47,6 @@
     1.4  [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
     1.5  
     1.6  # build args and nice setup for different target platforms
     1.7 -BUILD_OPTS=""
     1.8  BUILD_ARGS="-v"
     1.9  NICE="nice"
    1.10  case $HOSTNAME in
    1.11 @@ -69,7 +68,7 @@
    1.12  if [ "$1" = "-x" ]; then
    1.13    shift
    1.14    [ "$#" -lt 2 ] && usage
    1.15 -  BUILD_OPTS="$BUILD_OPTS -x $1"
    1.16 +  BUILD_ARGS="$BUILD_ARGS -x $1"
    1.17    shift
    1.18  fi
    1.19  
    1.20 @@ -130,7 +129,7 @@
    1.21  
    1.22      cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
    1.23      cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    1.24 -    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_OPTS -- $BUILD_ARGS >> $TESTLOG 2>&1)
    1.25 +    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
    1.26  
    1.27      if [ $? -eq 0 ]
    1.28      then