diff options
author | Frediano Ziglio <freddy77@gmail.com> | 2021-08-27 08:09:53 +0100 |
---|---|---|
committer | Frediano Ziglio <freddy77@gmail.com> | 2021-08-27 08:17:42 +0100 |
commit | d0d61488172c383fbaf4a6ab3de812f6a1376ac1 (patch) | |
tree | 391b36ca09a70a052d6510de1ed5ea7dd2ff2ea9 | |
parent | 81250a826e1cf935fa2e0234c4ab3fb0a615ef7d (diff) |
Minor updates
- add format for Vim
- remove previous error log before compiling the branch
- check for error pushing the branch
-rwxr-xr-x | spice-server/rebase | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/spice-server/rebase b/spice-server/rebase index a7501d0..93485c2 100755 --- a/spice-server/rebase +++ b/spice-server/rebase @@ -1,5 +1,7 @@ #!/bin/bash +# vim:ts=4:sw=4:expandtab: + # script to help rebase trees of branches # Git configuration # ----------------- @@ -109,6 +111,7 @@ try_compile() { echo "processed:$processed" echo "failed:$failed_compile" echo "compiling $branch ..." + rm -f compile_err_$branch.txt if test $COMPILE = full; then for commit in $(git rev-list ${REBASE_TO}..$branch --reverse); do echo "checking branch $branch commit $commit" @@ -190,6 +193,7 @@ do git checkout "$branch" if git rebase ${REBASE_TO}; then post_process "$branch" + set -e # if there is a remote on the git remote specified push to it if branch_need_push "$branch"; then echo "Pushing branch $branch ..." |