use MCS verified config if available

Signed-off-by: Axel Heider <axelheider@gmx.de>
seL4 · Jan 9, 2024 · dbb9677 · dbb9677
1 parent c92fde6
commit dbb9677
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/standalone-kernel/compile_kernel.sh b/standalone-kernel/compile_kernel.sh
@@ -72,7 +72,14 @@ do_compile_kernel()
             MCS)
                 build_folder="${build_folder}-${variant}"
                 variant_info=" (${variant})"
-                extra_params="${extra_params} -DKernelIsMCS=TRUE"
+                # Use a dedicated config file if available, otherwise just use
+                # the default config and enable MCS.
+                try_config_file="configs/${INPUT_ARCH}_MCS_verified.cmake"
+                if [ -f "${try_config_file}" ]; then
+                    config_file=${try_config_file}
+                else
+                    extra_params="${extra_params} -DKernelIsMCS=TRUE"
+                fi
                 ;;
             *)
                 echo "Unknown variant '${variant}'"