On Thu, Aug 30, 2018 at 12:36 AM, Ming Lin <min...@gmail.com> wrote: > Hi Sergey, > > Could you take a look at these 2 PRs?
Ping ... > > MDEV-16768: https://github.com/MariaDB/server/pull/837 > You approved this one, but not merged yet. > > MDEV-15816: https://github.com/MariaDB/server/pull/849 > This one was already merged by facebook. > > Thanks, > Ming _______________________________________________ Mailing list: https://launchpad.net/~maria-developers Post to : maria-developers@lists.launchpad.net Unsubscribe : https://launchpad.net/~maria-developers More help : https://help.launchpad.net/ListHelp