On Sat, Jan 09, 2021 at 05:15:12PM +0100, Roland Illig wrote: > I guess a simple "make clean && make" will clear up the situation.
Not quite, "make clean" will not remove the old ops.c file in the objdir,
you need to manually kill it (or just remove all lint objdirs completely).
Please add an entry to src/UPDATING, I would suggest something like:
find $OBJDIR -type d -name \*lint\* | xargs rm -rf
Martin
