On Tue, Jun 12, 2018 at 7:00 AM Gyan Doshi <gyandoshi at gmail.com> wrote: > > > Will push tomorrow. This flag is part of the public API, and eventhough it is entirely unused, you cannot remove public API without a proper deprecation period. - Hendrik