changeset 13839 | e1240620f1b5 |
parent 13680 | a6ce43a59d4a |
child 13900 | 0cfdeb44621e |
--- 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