author | wenzelm |
Sun, 19 Jun 2011 21:38:48 +0200 | |
changeset 43461 | d5187dd0e5fa |
parent 43460 | 2852f309174a |
child 43462 | 7f65a68f8b26 |
--- a/Admin/isatest/isatest-makedist Sun Jun 19 21:34:55 2011 +0200 +++ b/Admin/isatest/isatest-makedist Sun Jun 19 21:38:48 2011 +0200 @@ -59,7 +59,7 @@ echo "### building distribution" >> $DISTLOG 2>&1 mkdir -p $DISTPREFIX -$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110618" >> $DISTLOG 2>&1 +$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110619" >> $DISTLOG 2>&1 if [ $? -ne 0 ] then