Re: [#156] Pushing HEAD

Yes, we want to be able to do that!
-=R
On Jul 1, 2013 4:55 PM, "Martin Thomson" <martin.thomson@gmail.com> wrote:

> James tried to sneak in the ability to use server push for HEAD in
> #151. I backed out those changes, but I do think that we do want to do
> this. I just need a clear signal that we have consensus to add the
> feature.
>
> p.s. this wont make it into -04
> p.p.s. github is super-unicorny today \:-(
>
>