1
0
mirror of https://github.com/MariaDB/server.git synced 2025-08-08 11:22:35 +03:00

Merge branch '10.2' of github.com:MariaDB/server into bb-10.2-mariarocks-merge

This commit is contained in:
Sergei Petrunia
2017-09-19 15:34:38 +03:00
2312 changed files with 188819 additions and 61333 deletions

View File

@@ -1029,6 +1029,7 @@ public:
interface Rdb_tables_scanner {
virtual int add_table(Rdb_tbl_def * tdef) = 0;
virtual ~Rdb_tables_scanner() {} /* Keep the compiler happy */
};
/*