diff --git a/src/kernel_internals/runtime/fc_config.ml.in b/src/kernel_internals/runtime/fc_config.ml.in index 46be5ea3cfeeb6a30ef3bc85bb3f1d2986992f6d..87f0704a7d164674452601985c9a7af57d8d2443 100644 --- a/src/kernel_internals/runtime/fc_config.ml.in +++ b/src/kernel_internals/runtime/fc_config.ml.in @@ -37,6 +37,9 @@ let datadir = List.hd (List.rev datadirs) let plugin_dir = List.map Filepath.Normalized.of_string Config_data.Sites.plugins +let plugin_path = + String.concat ":" (Filepath.Normalized.to_string_list plugin_dir) + let framac_libc = Filepath.Normalized.concat datadir "libc" let () = Filepath.add_symbolic_dir_list "FRAMAC_SHARE" datadirs diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli index ad676f2371e9bfa4aa5620ecc54be063bd71bd4c..8be24f24b75a73c5cb65f11bfcad0f42f2a5f4cc 100644 --- a/src/kernel_internals/runtime/fc_config.mli +++ b/src/kernel_internals/runtime/fc_config.mli @@ -64,6 +64,10 @@ val framac_libc: Filepath.Normalized.t val plugin_dir: Filepath.Normalized.t list (** Directory where the Frama-C dynamic plug-ins are. *) +val plugin_path: string +(** The colon-separated concatenation of [plugin_dir]. + @since Magnesium-20151001 *) + val preprocessor: string (** Name of the default command to call the preprocessor. If the CPP environment variable is set, use it diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml index d700d9d07fe2ce440fbbeaa4e8e844e907252d2d..8aa896f86a21edce59881b558c3f37b67a56d965 100644 --- a/src/kernel_internals/runtime/special_hooks.ml +++ b/src/kernel_internals/runtime/special_hooks.ml @@ -70,6 +70,10 @@ let () = Cmdline.run_after_early_stage print_sharepath let print_libpath = print_configl Kernel.PrintLib.get Fc_config.plugin_dir let () = Cmdline.run_after_early_stage print_libpath +let print_pluginpath = + print_config Kernel.PrintPluginPath.get Fc_config.plugin_path +let () = Cmdline.run_after_early_stage print_pluginpath + (**************************************************************************) (* Hooks run after loading plug-ins *) (**************************************************************************)