On Wed Sep 14 16:03:35 2022 +0000, Julian Klemann wrote:
Well it didn't run my tests for me when I pulled your commits, even after rerunning configure, so I put it back and was already pushing when saw I your reply. If you need me to remove it I can I guess. I committed it previously because I just looked at a time a test was added and that happened so I just copied what it did.
It's probably fine to keep it as the change is small. Usually it's avoided so that `configure` is always generated by the maintainer and always with the same `autoconf` version. When working on a change locally you have to run either `autoreconf`, or `tools/make_makefiles` before building (like the gitlab CI does).