equal
deleted
inserted
replaced
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/isatool version` make) |
100 (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool getenv 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 |