Admin/isatest-makeall
changeset 13838 fe83f2231767
parent 13432 470daa444967
child 13901 af38553e61ee
equal deleted inserted replaced
13837:8dd150d36c65 13838:fe83f2231767
     6 #
     6 #
     7 # DESCRIPTION: Run isatool makeall from specified distribution and settings.
     7 # DESCRIPTION: Run isatool makeall from specified distribution and settings.
     8 #              Send email if it fails.
     8 #              Send email if it fails.
     9 
     9 
    10 ## global settings
    10 ## global settings
    11 MAILTO="kleing@in.tum.de nipkow@in.tum.de wenzelm@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
    11 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
    12 
    12 
    13 LOGPREFIX=~/log
    13 LOGPREFIX=~/log
    14 
    14 
    15 MASTERLOG=$LOGPREFIX/isatest.log
    15 MASTERLOG=$LOGPREFIX/isatest.log
    16 
    16 
    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 case $HOSTNAME in
       
    55         atbroy51)
       
    56 	MFLAGS="-j 2"
       
    57 	# MFLAGS=""
       
    58 	;;
       
    59 
       
    60         atbroy31)
       
    61         MFLAGS="-j 5"
       
    62         ;;
       
    63 	
       
    64 	atbroy12)
       
    65 	MFLAGS="-j 5"
       
    66 	;;
       
    67 
       
    68 	sunbroy2)
       
    69 	MFLAGS="-j 4"
       
    70 	;;
       
    71 
       
    72    	*)
       
    73 	MFLAGS=""
       
    74         ;;
       
    75 esac
       
    76 
       
    77 
       
    78 
    54 LOGS=""
    79 LOGS=""
    55 
    80 
    56 for SETTINGS in $@; do
    81 for SETTINGS in $@; do
    57 
    82 
    58     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    83     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    67     # the test
    92     # the test
    68 
    93 
    69     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
    94     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
    70 
    95 
    71     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    96     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    72     nice $DISTPREFIX/Isabelle/bin/isatool makeall -j 2 all >> $TESTLOG 2>&1 
    97     nice $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
    73 
    98 
    74     if [ $? -eq 0 ]
    99     if [ $? -eq 0 ]
    75     then
   100     then
    76         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   101         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
    77         gzip -f $TESTLOG
   102         gzip -f $TESTLOG