generate nightly devel snapshot
authorisatest
Fri Feb 28 14:25:22 2003 +0100 (2003-02-28)
changeset 13839e1240620f1b5
parent 13838 fe83f2231767
child 13840 399c8103a98f
generate nightly devel snapshot
Admin/isatest-makedist
     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