Peter Geoghegan <pg@bowt.ie> writes:
> The convention seems to be that it is located in the top-level
> directory. ISTM that we should follow that convention, since following
> the convention is good, and does not in itself force anybody to ignore
> any of the listed commits. Any thoughts on that?
Agreed. I think I'd previously suggested something under src/tools,
but we might as well do like others are doing; especially since
we have .gitattributes and the like there already.
regards, tom lane