On Fri, Jan 22, 2021 at 7:07 PM Tom Lane <t...@sss.pgh.pa.us> wrote: > > Daniel Gustafsson <dan...@yesql.se> writes: > >> 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". > > I found man pages for mkid online --- it's apparently a ctags-like > code indexing tool, not something for patches. So maybe Bruce still > uses it, or maybe not. But as long as we've also got make_ctags and > make_etags in there, I don't have a problem with leaving make_mkid. > > make_diff, on the other hand, certainly looks like technology whose > time has passed. I wonder about pgtest, too.
I'll go kill make_diff then -- quicker than fixing the docs of it. As for pgtest, that one looks a bit interesting as well -- but it's been patched on as late as 9.5 and in 2018, so it seems at least Bruce uses it :) While at it, what point is "codelines" adding? -- Magnus Hagander Me: https://www.hagander.net/ Work: https://www.redpill-linpro.com/
