On 2019-02-09 8:28 p.m., Robert Edmonds wrote: > Probably it's better to use the --with-chroot-dir= argument to configure > rather than directly patching the source to change the default.
Indeed and that's what's being proposed in the merge request. Regards, Simon