We don't want to include the header in the GitHub releases, as we will
end up with two headers with the same value. Considering that we are
thinking of fully automating patch releases, this change helps with that
too. Small steps.
Signed-off-by: Gerhard Lazu <gerhard@lazu.co.uk>
Keeping them in this repo might encourage more people to update
them as changes are merged, and simplify release automation a bit.
So let's try it. Per suggestion from @gerhard.
Michael Klishin
Gerhard Lazu