Hi, Here are two PRs that have already two approvals, yet they have not been merged for many weeks. Can you please state explicitly on the PR as a comment what the submitter needs to do, or if there is nothing to do, just merge it?
* https://github.com/MariaDB/server/pull/3208 * https://github.com/MariaDB/server/pull/2556 Thanks _______________________________________________ developers mailing list -- developers@lists.mariadb.org To unsubscribe send an email to developers-le...@lists.mariadb.org
