# HG changeset patch
# User wenzelm
# Date 1436952351 -7200
# Node ID 6d500a224cbe941068bfb92e501dd5ee4f709689
# Parent  daf200e2d79ab2b30aed43b4668429b38a0fc55d
back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc);

diff -r daf200e2d79a -r 6d500a224cbe Admin/isatest/isatest-makeall
--- 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