1.1 --- a/Admin/isatest/isatest-check Sat Oct 04 16:19:49 2008 +0200
1.2 +++ b/Admin/isatest/isatest-check Sat Oct 04 17:40:56 2008 +0200
1.3 @@ -97,7 +97,7 @@
1.4 # generate development snapshot page only for successful tests
1.5 # (failures in experimental sessions ok)
1.6 if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
1.7 - (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool getenv ISABELLE_IDENTIFIER` make)
1.8 + (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv ISABELLE_IDENTIFIER` make)
1.9 echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
1.10 fi
1.11