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