Patch: re-run make headers

[Dave Korn]

On 16/06/2010 19:34, Tom Tromey wrote:
> I happened to notice that re-running "make headers" causes a change.
> I guess someone forgot to run it in the past.
> 
> Ok?

  Isn't regenerating an autogenerated file always "obvious"?  Particularly in
this case where the changes are utterly non-functional.

    cheers,
      DaveK