Pushed to master as 170cb4c881..19528e39bb, with new make-flag. Thanks!

Regards,
RG.