-
Robert Schmidt authored
Instead of using ninja/make directly, there is a cmake command option to trigger the build using whatever build tool has been configured. Use it; if there is a mismatch, there will also be a clearer cmake error. Remove build_oai's --build-coverity: we don't use it, and it can trivially be added if required (probably, most users would run it by hand anyway). Add an error if the compilations function is not called with the right noumber of arguments.
4db08dc6