dev-build.py: don't require `time`

Knowing how much time the `make` subcommand took is but a nicety.