author | wenzelm |
Sat, 18 Jun 2011 17:42:28 +0200 | |
changeset 43444 | f744902b4681 |
parent 43443 | 5d9693c2337e |
child 43445 | 270bbbcda059 |
--- a/Admin/isatest/isatest-makedist Sat Jun 18 17:33:27 2011 +0200 +++ b/Admin/isatest/isatest-makedist Sat Jun 18 17:42:28 2011 +0200 @@ -59,7 +59,7 @@ echo "### building distribution" >> $DISTLOG 2>&1 mkdir -p $DISTPREFIX -$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110521" >> $DISTLOG 2>&1 +$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110618" >> $DISTLOG 2>&1 if [ $? -ne 0 ] then