removed doc/pick.sh, pointless to have it there

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