# HG changeset patch
# User isatest
# Date 1046438722 -3600
# Node ID e1240620f1b5cc9b4573e028582a26ce5d4b47f7
# Parent  fe83f22317678368dd1b12423835bafefb23c59e
generate nightly devel snapshot

diff -r fe83f2231767 -r e1240620f1b5 Admin/isatest-makedist
--- a/Admin/isatest-makedist	Fri Feb 28 14:11:54 2003 +0100
+++ b/Admin/isatest-makedist	Fri Feb 28 14:25:22 2003 +0100
@@ -87,6 +87,9 @@
 cd $DISTPREFIX >> $DISTLOG 2>&1
 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
 
+echo "### generating development snapshot web page" >> $DISTLOG 2>&1
+(cd ~/devel-page; make)
+
 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
 gzip -f $DISTLOG