1
0
mirror of https://github.com/MariaDB/server.git synced 2025-07-30 16:24:05 +03:00

rename maria to aria

This commit is contained in:
Sergei Golubchik
2010-09-12 18:40:01 +02:00
parent fa5baa12bc
commit e246077bcf
122 changed files with 2619 additions and 2616 deletions

View File

@ -44,17 +44,17 @@ try
case "EMBED_MANIFESTS":
case "EXTRA_DEBUG":
case "WITH_EMBEDDED_SERVER":
case "WITHOUT_MARIA_TEMP_TABLES":
case "WITHOUT_ARIA_TEMP_TABLES":
configfile.WriteLine("SET (" + args.Item(i) + " TRUE)");
break;
case "WITH_MARIA_STORAGE_ENGINE":
case "WITH_ARIA_STORAGE_ENGINE":
configfile.WriteLine("SET (" + args.Item(i) + " TRUE)");
if(with_maria_tmp_tables == -1)
{
with_maria_tmp_tables = 1;
}
break;
case "WITH_MARIA_TMP_TABLES":
case "WITH_ARIA_TMP_TABLES":
with_maria_tmp_tables = ( parts.length == 1 ||
parts[1] == "YES" || parts[1] == "TRUE");
break;
@ -73,7 +73,7 @@ try
}
if (with_maria_tmp_tables == 1)
{
configfile.WriteLine("SET (WITH_MARIA_TMP_TABLES TRUE)");
configfile.WriteLine("SET (WITH_ARIA_TMP_TABLES TRUE)");
}
if (actual_port == 0)
{