Admin/isatest/isatest-check
changeset 28508 e8197ea2703b
parent 28504 7ad7d7d6df47
child 28526 a30b9cf3502e
equal deleted inserted replaced
28507:325592dad134 28508:e8197ea2703b
    95 fi
    95 fi
    96 
    96 
    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 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 fi
   102 fi
   103 
   103 
   104 exit 0
   104 exit 0
   105 ## end
   105 ## end