Garbled output

With the new build system, the output of commands and the CI infrastructure can sometimes get garbled:

https://gitlab.idiap.ch/bob/bob.devtools/-/jobs/154891

It would be nice to fix this.