equal
deleted
inserted
replaced
58 echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1 |
58 echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1 |
59 rm -rf $HOME/isabelle-* |
59 rm -rf $HOME/isabelle-* |
60 |
60 |
61 echo "### building distribution" >> $DISTLOG 2>&1 |
61 echo "### building distribution" >> $DISTLOG 2>&1 |
62 mkdir -p $DISTPREFIX |
62 mkdir -p $DISTPREFIX |
63 $MAKEDIST -D -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1 |
63 $MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1 |
64 |
64 |
65 if [ $? -ne 0 ] |
65 if [ $? -ne 0 ] |
66 then |
66 then |
67 echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
67 echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
68 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
68 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |