diff options
| -rwxr-xr-x | doc/pick.sh | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/doc/pick.sh b/doc/pick.sh deleted file mode 100755 index e5f18da4..00000000 --- a/doc/pick.sh +++ /dev/null @@ -1,25 +0,0 @@ -#!/bin/bash - -# I work on a branch (named hut) which contains commits -# that should not be part of the standard distribution. -# -# This script picks all the good commits from hut and -# adds them to the master branch. -# Bad commits are marked with a "custom:" at the beginning -# of the commit message. - -MASTER_BRANCH='master' -CUSTOM_BRANCH='hut' -ORIGINAL_BRANCH=`git branch 2>/dev/null|grep -e ^* | tr -d \*\ ` - -git checkout -m $MASTER_BRANCH - -while read -r hash tag rest; do - if [ $tag != 'custom:' ]; then - git cherry-pick $hash || exit 1 - fi -done < <(git log --oneline --no-color $MASTER_BRANCH..$CUSTOM_BRANCH | tac) - -git checkout -m $CUSTOM_BRANCH -git rebase $MASTER_BRANCH -git checkout -m $ORIGINAL_BRANCH |