equal
deleted
inserted
replaced
57 rm -rf $HOME/isabelle-* |
57 rm -rf $HOME/isabelle-* |
58 ssh atbroy102 "rm -rf /home/isatest/isabelle-cygwin-poly-e" |
58 ssh atbroy102 "rm -rf /home/isatest/isabelle-cygwin-poly-e" |
59 |
59 |
60 echo "### building distribution" >> $DISTLOG 2>&1 |
60 echo "### building distribution" >> $DISTLOG 2>&1 |
61 mkdir -p $DISTPREFIX |
61 mkdir -p $DISTPREFIX |
62 $MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110622" >> $DISTLOG 2>&1 |
62 $MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20111217" >> $DISTLOG 2>&1 |
63 |
63 |
64 if [ $? -ne 0 ] |
64 if [ $? -ne 0 ] |
65 then |
65 then |
66 echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
66 echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
67 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
67 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |