Re: remove pgrminclude?

On 09.12.24 18:20, Tom Lane wrote:
> Peter Eisentraut <peter@eisentraut.org> writes:
>> I propose to remove the pgrminclude scripts and annotations.  AFAICT,
>> per git log, the last time someone tried to do something with it was
>> around 2011.  Also, many (not all) of the "pgrminclude ignore"
>> annotations are of a newer date but seem to have just been copied around
>> during refactorings and file moves and don't seem to reflect an actual
>> need anymore.
> 
> I agree with dropping pgrminclude --- as you say, it's not been used
> since 2011 and there seems little appetite for ever using it again.

committed