Merge with master.

This merges commit
bfe19f876cb20bea606e1a698030c017f31965c1
from master into our head commit
7a59013290bb26b80c997e5698757a735f1a92e0

Sincerely,
jit-merge command.

diff --git a/git-reset-script b/git-reset-script
index 0c02aa6423ec485e19bd7439c926addbb8fd029d..b6476edc30b9e8f7c991ebd9e25b530ec49b8253 100755 (executable)
--- a/git-reset-script
+++ b/git-reset-script
@@ -1,5 +1,7 @@
 #!/bin/sh
 . git-sh-setup-script || die "Not a git archive"
-git-read-tree --reset HEAD
+rev=$(git-rev-parse --revs-only --verify --default HEAD "$@") || exit
+rev=$(git-rev-parse --revs-only --verify $rev^0) || exit
+git-read-tree --reset "$rev" && echo "$rev" > "$GIT_DIR/HEAD"
 git-update-cache --refresh
 rm -f "$GIT_DIR/MERGE_HEAD"