blob: c54582590f3003ed3c1841222b71e166fca33933 (
plain)
1
2
3
4
5
6
7
8
9
10
|
#!/bin/bash -e
# Copy your current branch to a "publishing" remote.
#
# By default, this remote is the remote matching your local username. However,
# you can set `publish.remote` to publish to another repository (eg. origin).
REMOTE="$(git config publish.remote || echo "${USER}")"
exec git push --force-with-lease "$@" "${REMOTE}" HEAD
|
