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 -- Sent via pgsql-hackers mailing list (pgsql-hackers@postgresql.org) To make changes to your subscription: http://www.postgresql.org/mailpref/pgsql-hackers
