Re: mkid reference

> On 22 Jan 2021, at 12:56, Magnus Hagander <magnus@hagander.net> wrote:

> And maybe even more interestnig -- is there a point to this whole
> make_diff directory at all in these days of git? Or should we just
> remove it rather than try to fix it?

There's also src/tools/make_mkid which use this mkid tool.  +1 for removing.
If anything, it seems better replaced by extended documentation on the existing
wiki article [0] on how to use "git format-patch".

--
Daniel Gustafsson        https://vmware.com/

[0] https://wiki.postgresql.org/wiki/Working_with_Git