github_pull.sh

#!/bin/bash
GITHUB_USER="madmax"

if [ "$1" != "" ]; then
  echo "Merging pull request $1"
  OUT=`basename $1`
  curl --user $GITHUB_USER $1.patch > $OUT.patch 
  git am -s --3way --ignore-space-change $OUT.patch
  rm $OUT.patch
else
  echo "No parameters given, exiting..."
  echo ""
  echo "Usage: $0 <url>"
  exit 1

fi