Skip to content

Makefile: fix recursive invocation to use `$(MAKE)`

Paolo G. Giarrusso requested to merge Blaisorblade/iris:fix-makefile into master

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

Merge request reports