[PATCH] hgweb: add HEAD method

[Greg Ward]

On Sun, Apr 12, 2009 at 6:40 AM, Alexander Solovyov
<piranha at piranha.org.ua> wrote:
> # HG changeset patch
> # User Alexander Solovyov <piranha at piranha.org.ua>
> # Date 1239532688 -10800
> # Node ID aaaa7731388e39b7bf43aac5ed3d82bf9a2784df
> # Parent  fe2a87a3d344878982641110dd26f2949a0b6fff
> hgweb: add HEAD method
>
> This fixes wget when it tries to determine filename by issuing a HEAD request
> first.
>
> diff --git a/mercurial/hgweb/server.py b/mercurial/hgweb/server.py
> --- a/mercurial/hgweb/server.py
> +++ b/mercurial/hgweb/server.py
> @@ -75,6 +75,9 @@ class _hgwebhandler(object, BaseHTTPServ
>     def do_GET(self):
>         self.do_POST()
>
> +    def do_HEAD(self):
> +        self.do_POST()
> +

But... ummm... doesn't that make hgweb issue a response with a body,
which is exactly what HEAD is not supposed to do?  Or does the
framework that imposes the do_{GET,HEAD,POST} convention take care of
that by not sending the body?

Greg