Configuration file: new default value for GlobalInitFile option

If the user did not specify the GlobalInitFile option, use global_init.m in configuration
directory if it exists.
master
Sébastien Villemot 2023-12-12 16:01:54 +01:00
parent 1de83b7b12
commit cd86b1895d
No known key found for this signature in database
GPG Key ID: 2CECE9350ECEBE4A
1 changed files with 6 additions and 0 deletions

View File

@ -647,6 +647,12 @@ Configuration::checkPass([[maybe_unused]] WarningConsolidation& warnings) const
void
Configuration::transformPass()
{
/* If the user did not specify the GlobalInitFile option, use global_init.m in configuration
directory if it exists */
if (auto default_global_init_file = findConfigFile("global_init.m");
global_init_file.empty() && !default_global_init_file.empty())
global_init_file = default_global_init_file.string();
if (!parallel && !parallel_test)
return;