Admin/isatest-makeall
changeset 13987 31891dd8c04b
parent 13985 3852929a8d1d
child 13990 506102b6a6d4
equal deleted inserted replaced
13986:d2fd7deceaa6 13987:31891dd8c04b
    99     SHORT=${SETTINGS##*/}
    99     SHORT=${SETTINGS##*/}
   100     TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
   100     TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
   101 
   101 
   102     # the test
   102     # the test
   103 
   103 
   104     touch $RUNNING/$SHORT
   104     touch $RUNNING/$SHORT.running
   105 
   105 
   106     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   106     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   107 
   107 
   108     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   108     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   109     $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   109     $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   126         echo >> $ERRORLOG
   126         echo >> $ERRORLOG
   127 
   127 
   128         FAIL="$FAIL$SHORT "
   128         FAIL="$FAIL$SHORT "
   129     fi
   129     fi
   130 
   130 
   131     rm -f $RUNNING/$SHORT
   131     rm -f $RUNNING/$SHORT.running
   132 done
   132 done
   133 
   133 
   134 # time and success/failure to master log
   134 # time and success/failure to master log
   135 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   135 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   136 
   136