author | wenzelm |
Mon, 20 Jun 2011 22:48:41 +0200 | |
changeset 43483 | a7a8496d3bfc |
parent 43482 | ebb90ff55b79 |
child 43484 | 51b8043a8cf5 |
--- a/Admin/isatest/isatest-makedist Mon Jun 20 22:43:56 2011 +0200 +++ b/Admin/isatest/isatest-makedist Mon Jun 20 22:48:41 2011 +0200 @@ -59,7 +59,7 @@ echo "### building distribution" >> $DISTLOG 2>&1 mkdir -p $DISTPREFIX -$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110619" >> $DISTLOG 2>&1 +$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110620" >> $DISTLOG 2>&1 if [ $? -ne 0 ] then