On 09.01.2021 17:42, Martin Husemann wrote:
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
Thanks for the suggestion, I first did that. I was unsatisfied though that people would actively have to read src/UPDATING. Therefore, after reproducing the problem locally, I renamed ops.c to oper.c, after which the build ran successfully. Roland