review-pr

# Shell function to pull a PR into a branch to study it locally
# ...original from unkonwn source (but probably from GitHub documentation)

review_pr () 
{ 
    [ -z "$1" ] && { 
        echo "reviewpull <pull-request-number>";
        return 1
    };
    echo "git fetch origin pull/$1/head:pr_$1"
    git fetch origin pull/$1/head:pr_$1
    echo "git checkout pr_$1"
    git checkout pr_$1
}