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