Yes these patches can be cherry-picked.

git cherry-pick 17262470246232d0f0651d627a4961e55b1efe6a
git cherry-pick 99febe7fd50c31c0f5dd40fa7f376f2c1f64f8c3

I will try this now and will compile.

- Sunil
On Fri, Jul 6, 2018 at 10:59 AM Giovanni Matteo Fumarola <
[EMAIL PROTECTED]> wrote: