Add support for pushing to a remote repository using HTTP/DAV

diff --git a/git-fetch.sh b/git-fetch.sh
index 7c05880bcfca30426d03112c0967ada6f68305be..31e5f4c7225df3d279b78f67ebd0f7a8c87ede40 100755 (executable)
--- a/git-fetch.sh
+++ b/git-fetch.sh
@@ -114,7 +114,12 @@ fast_forward_local () {
        # is no way to guarantee "fast-forward" anyway.
        if test -f "$GIT_DIR/$1"
        then
-               echo >&2 "* $1: updating with $3"
+               if now_=$(cat "$GIT_DIR/$1") && test "$now_" = "$2"
+               then
+                       echo >&2 "* $1: same as $3"
+               else
+                       echo >&2 "* $1: updating with $3"
+               fi
        else
                echo >&2 "* $1: storing $3"
        fi
@@ -176,6 +181,7 @@ if test "$tags"
 then
        taglist=$(git-ls-remote --tags "$remote" |
                sed -e '
+                       /\^/d
                        s/^[^   ]*      //
                        s/.*/&:&/')
        if test "$#" -gt 1