Admin/isatest/isatest-check
changeset 28439 a978bd4d956e
parent 25912 a1a3f614dd86
child 28504 7ad7d7d6df47
     1.1 --- a/Admin/isatest/isatest-check	Tue Sep 30 23:31:40 2008 +0200
     1.2 +++ b/Admin/isatest/isatest-check	Wed Oct 01 00:09:51 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 version` make)
     1.8 +  (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool getenv ISABELLE_IDENTIFIER` make)
     1.9    echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
    1.10  fi
    1.11