From cd86b1895d97d1b195849072a8d26fd372ca5d8c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?S=C3=A9bastien=20Villemot?= Date: Tue, 12 Dec 2023 16:01:54 +0100 Subject: [PATCH] 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. --- src/Configuration.cc | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Configuration.cc b/src/Configuration.cc index 85ed5482..247dbd5c 100644 --- a/src/Configuration.cc +++ b/src/Configuration.cc @@ -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;