Admin/isatest-makedist
changeset 13993 88a8911bb65d
parent 13991 b289ab046d3b
child 14032 a6239314e380
     1.1 --- a/Admin/isatest-makedist	Fri May 09 14:08:04 2003 +0200
     1.2 +++ b/Admin/isatest-makedist	Fri May 09 14:15:50 2003 +0200
     1.3 @@ -92,9 +92,6 @@
     1.4  cd $DISTPREFIX >> $DISTLOG 2>&1
     1.5  $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
     1.6  
     1.7 -echo "### generating development snapshot web page" >> $DISTLOG 2>&1
     1.8 -(cd $HOME/devel-page; make)
     1.9 -
    1.10  echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    1.11  gzip -f $DISTLOG
    1.12