Dont use "eval time", time depends on bash
eval will use /bin/sh to run the shell command, and on Debian/Ubuntu this points to dash, which does not have the time command Replaced with bash -c
Provided with 
eval will use /bin/sh to run the shell command, and on Debian/Ubuntu this points to dash, which does not have the time command Replaced with bash -c
enabled an automatic merge when the pipeline for 79e32ded succeeds
By Maxime Perrotin on 2020-05-29T10:08:46
mentioned in commit e80cca8b
By Maxime Perrotin on 2020-05-29T10:17:12
merged
By Maxime Perrotin on 2020-05-29T10:17:12
Provided with