Admin/isatest-makedist

--- a/Admin/isatest-makedist	Fri May 09 14:08:04 2003 +0200
+++ b/Admin/isatest-makedist	Fri May 09 14:15:50 2003 +0200
@@ -92,9 +92,6 @@
 cd $DISTPREFIX >> $DISTLOG 2>&1
 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
 
-echo "### generating development snapshot web page" >> $DISTLOG 2>&1
-(cd $HOME/devel-page; make)
-
 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
 gzip -f $DISTLOG