Tracing where build time is spent

[Stephan Bergmann]

On 16/02/2020 15:33, Luboš Luňák wrote:
> Also, now that we do have Jenkins builds, maybe finally plain 'make'
> could be sensible and not run tests all the time.
I'm all for that.  I think our default make target behavior and the 
build-nocheck target, both non-standard, are not too helpful overall. 
(Gerrit Jenkins builds that today use the default make target should 
then make sure they still run the tests they run today, by making 
whatever appropriate target instead.)