author | wenzelm |
Sat, 17 Dec 2011 16:24:14 +0100 | |
changeset 45913 | 7f7c3922c636 |
parent 45912 | 3d0416135efb |
child 45914 | eaf6728d2512 |
--- a/Admin/isatest/isatest-makedist Sat Dec 17 16:22:16 2011 +0100 +++ b/Admin/isatest/isatest-makedist Sat Dec 17 16:24:14 2011 +0100 @@ -59,7 +59,7 @@ echo "### building distribution" >> $DISTLOG 2>&1 mkdir -p $DISTPREFIX -$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110622" >> $DISTLOG 2>&1 +$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20111217" >> $DISTLOG 2>&1 if [ $? -ne 0 ] then