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 weshould put them.