From e2e31c3c84f0b7c95591a7d2244d7add345a442f Mon Sep 17 00:00:00 2001
From: hut <hut@lavabit.com>
Date: Wed, 31 Mar 2010 05:15:26 +0200
Subject: removed doc/pick.sh, pointless to have it there

---
 doc/pick.sh | 25 -------------------------
 1 file changed, 25 deletions(-)
 delete mode 100755 doc/pick.sh

(limited to 'doc')

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
-- 
cgit 1.4.1-2-gfad0