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/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 |