> 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