# HG changeset patch
# User kleing
# Date 1223205228 -7200
# Node ID e8197ea2703bb093c93c65da11793fd29cda400f
# Parent  325592dad1341fc97ec22576d004efc68cf68a47
needs -b option for isabelle getenv

diff -r 325592dad134 -r e8197ea2703b Admin/isatest/isatest-check
--- a/Admin/isatest/isatest-check	Sat Oct 04 17:51:10 2008 +0200
+++ b/Admin/isatest/isatest-check	Sun Oct 05 13:13:48 2008 +0200
@@ -97,7 +97,7 @@
 # generate development snapshot page only for successful tests
 # (failures in experimental sessions ok)
 if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
-  (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv ISABELLE_IDENTIFIER` make)
+  (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv -b ISABELLE_IDENTIFIER` make)
   echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
 fi