Peter Eisentraut wrote:
> On 6/19/13 12:20 PM, Andrew Dunstan wrote:
> > So you're saying to install extension headers, but into the main
> > directory where we put server headers?
>
> Yes, if we choose to install some extension headers, that is where we
> should put them.
The question of the name of the directory still stands. "contrib" would
be the easiest answer, but it's slightly wrong because
externally-supplied modules could also want to install headers.
"extension" might be it, but there are things that aren't extensions
(right? if not, that would be my choice).
--
Álvaro Herrera http://www.2ndQuadrant.com/
PostgreSQL Development, 24x7 Support, Training & Services