diff --git a/admin/environment.xml b/admin/environment.xml index 37916496422..834b0177082 100644 --- a/admin/environment.xml +++ b/admin/environment.xml @@ -4714,7 +4714,6 @@ - @@ -4892,8 +4891,6 @@ - - diff --git a/lib/environmentlib.php b/lib/environmentlib.php index 2dcd9fe4aa0..4abbdd82fe4 100644 --- a/lib/environmentlib.php +++ b/lib/environmentlib.php @@ -1053,15 +1053,16 @@ function environment_check_database($version, $env_select) { $dbinfo = $DB->get_server_info(); $current_version = normalize_version($dbinfo['version']); - $needed_version = $vendors[$current_vendor]; -/// Check we have a needed version - if (!$needed_version) { + // Check we have a needed version. + if (empty($vendors[$current_vendor])) { $result->setStatus(false); $result->setErrorCode(NO_DATABASE_VENDOR_VERSION_FOUND); return $result; } + $needed_version = $vendors[$current_vendor]; + // Check if the DB Vendor has been properly configured. // Hack: this is required when playing with MySQL and MariaDB since they share the same PHP module and base DB classes, // whilst they are slowly evolving using separate directions though MariaDB is still an "almost" drop-in replacement.