Merged requested to merge Blaisorblade/iris:fix-makefile into master
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: 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: Nothing to be done for `post-all'. make: *** wait: No child processes. Stop. gmake: *** [Makefile:3: all] Error 2