Admin/isatest-makeall
changeset 13924 09f6f2fefb25
parent 13901 af38553e61ee
child 13962 908f6776a59b
equal deleted inserted replaced
13923:019342d03d81 13924:09f6f2fefb25
    49 DISTPREFIX=$1
    49 DISTPREFIX=$1
    50 shift
    50 shift
    51 
    51 
    52 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    52 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    53 
    53 
       
    54 NICE=nice
       
    55 
    54 case $HOSTNAME in
    56 case $HOSTNAME in
    55         atbroy51)
    57         atbroy51)
    56 	MFLAGS="-j 2"
    58 	MFLAGS="-j 2"
    57 	# MFLAGS=""
    59 	# MFLAGS=""
       
    60   NICE=""
    58 	;;
    61 	;;
    59 
    62 
    60         atbroy31)
    63         atbroy31)
    61         MFLAGS="-j 5"
    64         MFLAGS="-j 5"
    62         ;;
    65         ;;
    96     # the test
    99     # the test
    97 
   100 
    98     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   101     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
    99 
   102 
   100     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   103     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   101     nice $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   104     $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   102 
   105 
   103     if [ $? -eq 0 ]
   106     if [ $? -eq 0 ]
   104     then
   107     then
   105         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   108         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   106         gzip -f $TESTLOG
   109         gzip -f $TESTLOG