more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
--- a/Admin/isatest/isatest-makeall Wed Dec 28 13:00:51 2011 +0100
+++ b/Admin/isatest/isatest-makeall Wed Dec 28 13:08:18 2011 +0100
@@ -71,7 +71,6 @@
macbroy2)
MFLAGS="-k"
- TARGETS=full
NICE=""
;;
@@ -102,7 +101,6 @@
macbroy30)
MFLAGS="-k"
- TARGETS=full
NICE=""
;;
@@ -124,8 +122,13 @@
TARGETS="$2"
shift 2
ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
- DIR="$ISABELLE_HOME/src/$LOGIC"
- TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
+ if [ "$LOGIC" = "." ]; then
+ DIR="."
+ TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
+ else
+ DIR="$ISABELLE_HOME/src/$LOGIC"
+ TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
+ fi
else
DIR="."
TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
--- a/Admin/isatest/isatest-makedist Wed Dec 28 13:00:51 2011 +0100
+++ b/Admin/isatest/isatest-makedist Wed Dec 28 13:08:18 2011 +0100
@@ -107,7 +107,11 @@
sleep 15
$SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8; $MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
+$SSH macbroy2 "
+ $MAKEALL $HOME/settings/mac-poly64-M4 -l . full;
+ $MAKEALL $HOME/settings/mac-poly64-M8 -l . full;
+ $MAKEALL $HOME/settings/mac-poly-M4;
+ $MAKEALL $HOME/settings/mac-poly-M8"
sleep 15
$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
sleep 15