On Mon, Jan 9, 2023 at 2:18 PM Peter Geoghegan <pg@bowt.ie> wrote:
> I'll try to get back to it this week.
Attached patch fixes up these issues. It's almost totally mechanical.
(Ended up using "git diff --color-moved=dimmed-zebra
--color-moved-ws=ignore-all-space" with this, per your recent tip,
which did help.)
--
Peter Geoghegan