Admin/isatest/isatest-check
changeset 28539 bdb308737bfd
parent 28526 a30b9cf3502e
child 31582 4753c317d5c1
equal deleted inserted replaced
28538:3147236326ea 28539:bdb308737bfd
    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 -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   log "generated development snapshot web page."
   102 else
   102 else
   103   echo "$(date) $HOSTNAME $PRG: test failures, no web snapshot generated." >> $MASTERLOG
   103   log "test failures, no web snapshot generated."
   104 fi
   104 fi
   105 
   105 
   106 exit 0
   106 exit 0
   107 ## end
   107 ## end