David:
I believe that src/Makefile.inc1 needs a tweak to add "time" to the list
of "Required install tools to be saved in a scratch dir for safety"
This fix an issue introduced by 99feb137f5f66f903bba816c1d98ced2a92bef12
Differential D31373
add the time(1) command to the list of install tools wosch on Aug 1 2021, 12:41 PM. Authored by Tags None Referenced Files
Subscribers None
Details David: I believe that src/Makefile.inc1 needs a tweak to add "time" to the list This fix an issue introduced by 99feb137f5f66f903bba816c1d98ced2a92bef12
Diff Detail
Event TimelineComment Actions I committed the fix. Sorry for the short term notice, but given that some of our main jenkins jobs are not running there was some urgency. We can improve the fix later if you want. |