Admin/isatest/isatest-check
changeset 28526 a30b9cf3502e
parent 28508 e8197ea2703b
child 28539 bdb308737bfd
equal deleted inserted replaced
28525:42297ae4df47 28526:a30b9cf3502e
    46 
    46 
    47 ## main
    47 ## main
    48 
    48 
    49 # check if tests are still running, wait for them a couple of hours
    49 # check if tests are still running, wait for them a couple of hours
    50 i=0
    50 i=0
    51 while [ -n "$(ls $RUNNING)" -a $i -lt 10 ]; do 
    51 while [ -n "$(ls $RUNNING)" -a $i -lt 40 ]; do 
    52     sleep 3600
    52     sleep 900
    53     let "i = i+1"
    53     let "i = i+1"
    54 done
    54 done
    55 
    55 
    56 FAIL=0
    56 FAIL=0
    57 
    57 
    97 # generate development snapshot page only for successful tests
    97 # generate development snapshot page only for successful tests
    98 # (failures in experimental sessions ok)
    98 # (failures in experimental sessions ok)
    99 if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
    99 if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
   100   (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv -b ISABELLE_IDENTIFIER` make)
   100   (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv -b ISABELLE_IDENTIFIER` make)
   101   echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
   101   echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
       
   102 else
       
   103   echo "$(date) $HOSTNAME $PRG: test failures, no web snapshot generated." >> $MASTERLOG
   102 fi
   104 fi
   103 
   105 
   104 exit 0
   106 exit 0
   105 ## end
   107 ## end