If I am reading `Makefile` and `Makefile.build` correctly, running `make` runs `make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"` and the `world` target of `Makefile.build` is `world: revision coq coqide`, even if I `/.configure -local -coqide no`.  So I strongly suspect that `make coqide` will not die if we don't know how to build `coqide`.  I will test it on travis soon.