> On 22 Jan 2021, at 12:56, Magnus Hagander <mag...@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
