Admin/isatest/isatest-makedist
changeset 48790 6e739225dd8a
parent 48635 bfce940c6f38
child 48832 ab9663b8734b
     1.1 --- a/Admin/isatest/isatest-makedist	Mon Aug 13 20:31:24 2012 +0200
     1.2 +++ b/Admin/isatest/isatest-makedist	Tue Aug 14 10:44:03 2012 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  
     1.5  echo "### building distribution"  >> $DISTLOG 2>&1
     1.6  mkdir -p $DISTPREFIX
     1.7 -$MAKEDIST -D -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
     1.8 +$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
     1.9  
    1.10  if [ $? -ne 0 ]
    1.11  then