author | wenzelm |
Fri, 17 Aug 2012 10:46:42 +0200 | |
changeset 48832 | ab9663b8734b |
parent 48831 | 2cc51d1cabd7 |
child 48833 | 10584ca5785f |
child 48851 | 0cf8bc6f7084 |
--- a/Admin/isatest/isatest-makedist Thu Aug 16 17:19:48 2012 +0200 +++ b/Admin/isatest/isatest-makedist Fri Aug 17 10:46:42 2012 +0200 @@ -60,7 +60,7 @@ echo "### building distribution" >> $DISTLOG 2>&1 mkdir -p $DISTPREFIX -$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1 +$MAKEDIST -j "/home/isabelle/contrib/jedit_build-20120813" >> $DISTLOG 2>&1 if [ $? -ne 0 ] then