Makefile: fix recursive invocation to use `$(MAKE)`
Calling make
instead of $(MAKE)
is a known antipattern, but I thought it almost always works, if suboptimally.
Today I met a counterexample — I used the -O
option for buffering of parallel output (new in make 4!), and make got completely confused!
$ gmake -j5
[... works fine! ]
$ make clean
[...]
$ gmake -j5 -O
make[2]: Nothing to be done for `pre-all'.
touch theories/algebra/ofe.vo
touch theories/algebra/monoid.vo
touch theories/algebra/cmra.vo
[...]
touch theories/heap_lang/lib/array.vo
make[2]: Nothing to be done for `post-all'.
make[1]: *** wait: No child processes. Stop.
gmake: *** [Makefile:3: all] Error 2