1#!/usr/bin/env bash
2# Fetch any remote branches from the remote Git server.
3#
4# This includes removing any branches which have been deleted on the remote,
5# e.g. when a GitHub pull request is merged.
6
7set -o errexit
8set -o nounset
9
10_ensure_ssh_key_loaded
11
12print_info "-> git fetch origin --prune $@"
13git fetch origin --prune "$@"