diff options
Diffstat (limited to 'git-pull-script')
| -rwxr-xr-x | git-pull-script | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/git-pull-script b/git-pull-script index 7016fbf943..c31a65ca8c 100755 --- a/git-pull-script +++ b/git-pull-script @@ -5,7 +5,25 @@ # Fetch one or more remote refs and merge it/them into the current HEAD. . git-sh-setup-script || die "Not a git archive" -git-fetch-script "$@" || exit 1 + +orig_head=$(cat "$GIT_DIR/HEAD") || die "Pulling into a black hole?" +git-fetch-script --update-head-ok "$@" || exit 1 + +curr_head=$(cat "$GIT_DIR/HEAD") +if test "$curr_head" != "$orig_head" +then + # The fetch involved updating the current branch. + + # The working tree and the index file is still based on the + # $orig_head commit, but we are merging into $curr_head. + # First update the working tree to match $curr_head. + + echo >&2 "Warning: fetch updated the current branch head." + echo >&2 "Warning: fast forwarding your working tree." + git-read-tree -u -m "$orig_head" "$curr_head" || + die "You need to first update your working tree." +fi + merge_head=$(sed -e 's/ .*//' "$GIT_DIR"/FETCH_HEAD | tr '\012' ' ') merge_name=$(sed -e 's/^[0-9a-f]* //' "$GIT_DIR"/FETCH_HEAD | tr '\012' ' ') |