diff --git a/otherlibs/site/src/plugins/dune b/otherlibs/site/src/plugins/dune index 2f5beebe625e..d2bf4e079e21 100644 --- a/otherlibs/site/src/plugins/dune +++ b/otherlibs/site/src/plugins/dune @@ -6,4 +6,4 @@ (dune_site (plugins) (data_module dune_site_plugins_data))) - (libraries dune-site dune-private-libs.meta_parser dynlink)) + (libraries dune-site dune-private-libs.meta_parser linker)) diff --git a/otherlibs/site/src/plugins/linker/dune b/otherlibs/site/src/plugins/linker/dune new file mode 100644 index 000000000000..ce852a1e35b5 --- /dev/null +++ b/otherlibs/site/src/plugins/linker/dune @@ -0,0 +1,5 @@ +(library + (name linker) + (public_name dune-site.linker) + (virtual_modules linker) + (default_implementation dune-site.dynlink)) diff --git a/otherlibs/site/src/plugins/linker/dynlink/dune b/otherlibs/site/src/plugins/linker/dynlink/dune new file mode 100644 index 000000000000..603dbfa1845c --- /dev/null +++ b/otherlibs/site/src/plugins/linker/dynlink/dune @@ -0,0 +1,6 @@ +(library + (name dune_site_dynlink_linker) + (modes native) + (public_name dune-site.dynlink) + (implements dune-site.linker) + (libraries dynlink)) diff --git a/otherlibs/site/src/plugins/linker/dynlink/linker.ml b/otherlibs/site/src/plugins/linker/dynlink/linker.ml new file mode 100644 index 000000000000..73bf7a03a50f --- /dev/null +++ b/otherlibs/site/src/plugins/linker/dynlink/linker.ml @@ -0,0 +1 @@ +let load = Dynlink.loadfile diff --git a/otherlibs/site/src/plugins/linker/linker.mli b/otherlibs/site/src/plugins/linker/linker.mli new file mode 100644 index 000000000000..63fbb5a31860 --- /dev/null +++ b/otherlibs/site/src/plugins/linker/linker.mli @@ -0,0 +1 @@ +val load : string -> unit diff --git a/otherlibs/site/src/plugins/linker/toplevel/dune b/otherlibs/site/src/plugins/linker/toplevel/dune new file mode 100644 index 000000000000..c56cd49f8249 --- /dev/null +++ b/otherlibs/site/src/plugins/linker/toplevel/dune @@ -0,0 +1,6 @@ +(library + (name dune_site_toplevel_linker) + (modes byte) + (public_name dune-site.toplevel) + (implements dune-site.linker) + (libraries compiler-libs.toplevel)) diff --git a/otherlibs/site/src/plugins/linker/toplevel/linker.ml b/otherlibs/site/src/plugins/linker/toplevel/linker.ml new file mode 100644 index 000000000000..563590db4366 --- /dev/null +++ b/otherlibs/site/src/plugins/linker/toplevel/linker.ml @@ -0,0 +1 @@ +let load = Topdirs.dir_load Format.err_formatter diff --git a/otherlibs/site/src/plugins/plugins.ml b/otherlibs/site/src/plugins/plugins.ml index 581a8b9f803a..7d848890f7bd 100644 --- a/otherlibs/site/src/plugins/plugins.ml +++ b/otherlibs/site/src/plugins/plugins.ml @@ -256,7 +256,7 @@ let load_gen ~load_requires dirs name = List.iter (fun p -> let file = Filename.concat directory p in - Dynlink.loadfile file) + Linker.load file) plugins) let rec load_requires name =