--- a/Admin/isatest/isatest-makeall Tue Jul 14 19:08:40 2015 +0200
+++ b/Admin/isatest/isatest-makeall Wed Jul 15 11:25:51 2015 +0200
@@ -47,7 +47,6 @@
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
# build args and nice setup for different target platforms
-BUILD_OPTS=""
BUILD_ARGS="-v"
NICE="nice"
case $HOSTNAME in
@@ -69,7 +68,7 @@
if [ "$1" = "-x" ]; then
shift
[ "$#" -lt 2 ] && usage
- BUILD_OPTS="$BUILD_OPTS -x $1"
+ BUILD_ARGS="$BUILD_ARGS -x $1"
shift
fi
@@ -130,7 +129,7 @@
cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
- (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_OPTS -- $BUILD_ARGS >> $TESTLOG 2>&1)
+ (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
if [ $? -eq 0 ]
then