Teach git push .git/branches shorthand

diff --git a/git-fetch-script b/git-fetch-script
index a0326f0e789145ee93f188d5bb3855d8a029bd6b..24f0a5ec82e7268f6dcb0beefb6dbe0f7f54f463 100755 (executable)
--- a/git-fetch-script
+++ b/git-fetch-script
@@ -15,7 +15,7 @@ http://* | https://*)
         fi
        _x40='[0-9a-f][0-9a-f][0-9a-f][0-9a-f][0-9a-f]' &&
        _x40="$_x40$_x40$_x40$_x40$_x40$_x40$_x40$_x40" &&
-       head=$(curl -ns $curl_extra_args "$merge_repo/$merge_head") &&
+       head=$(curl -nsf $curl_extra_args "$merge_repo/$merge_head") &&
        expr "$head" : "$_x40\$" >/dev/null || {
                echo >&2 "Failed to fetch $merge_head from $merge_repo"
                exit 1