diff --git a/src/init/boot/dune b/src/init/boot/dune index efc35b44550f7dd6480f351b65583393b20b4ca6..2dd90880b34d919c0a1d8e5923d94ef48b388390 100644 --- a/src/init/boot/dune +++ b/src/init/boot/dune @@ -44,6 +44,7 @@ (executable (name empty_file) (public_name frama-c) + (modes byte (best exe)) (modules empty_file) (package frama-c) (flags :standard -open Frama_c_kernel -linkall) diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml index 9524edda4888b72a0e631cef9dddcf5890d1bc57..fe20f1848549c440da0d6a57421e2dd2ac1639f3 100644 --- a/src/kernel_services/plugin_entry_points/dynamic.ml +++ b/src/kernel_services/plugin_entry_points/dynamic.ml @@ -145,6 +145,14 @@ let load_module m = load_plugin m end +let () = Printexc.register_printer (function + | Dynlink.Error err -> Some (Dynlink.error_message err) + | _ -> None + ) + +let () = Dynlink.allow_unsafe_modules true + + (* ************************************************************************* *) (** {2 Registering and accessing dynamic values} *) (* ************************************************************************* *)