Admin/isatest-makedist
changeset 13839 e1240620f1b5
parent 13680 a6ce43a59d4a
child 13900 0cfdeb44621e
     1.1 --- a/Admin/isatest-makedist	Fri Feb 28 14:11:54 2003 +0100
     1.2 +++ b/Admin/isatest-makedist	Fri Feb 28 14:25:22 2003 +0100
     1.3 @@ -87,6 +87,9 @@
     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 ~/devel-page; make)
     1.9 +
    1.10  echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    1.11  gzip -f $DISTLOG
    1.12