diff options
Diffstat (limited to 'sysinit')
| -rw-r--r-- | sysinit/coqloadpath.ml | 14 | ||||
| -rw-r--r-- | sysinit/dune | 5 |
2 files changed, 14 insertions, 5 deletions
diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml index 8635345e00..95ae5da3de 100644 --- a/sysinit/coqloadpath.ml +++ b/sysinit/coqloadpath.ml @@ -44,8 +44,18 @@ let init_load_path ~coqlib = let coq_path = Names.DirPath.make [Libnames.coq_root] in (* ML includes *) - let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") |> List.map fst in - + let unix_path = + (* Usually lib/coq-stdlib/../plugins ; this kind of hacks with the + ML path should go away once we use ocamlfind to load plugins *) + CPath.choose_existing + [ CPath.make [ coqlib ; "plugins" ] + ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] + ] |> function + | None -> + CErrors.user_err (Pp.str "Cannot find plugins directory") + | Some f -> (f :> string) + in + let plugins_dirs = System.all_subdirs ~unix_path |> List.map fst in let contrib_ml, contrib_vo = build_userlib_path ~unix_path:user_contrib in let misc_ml, misc_vo = diff --git a/sysinit/dune b/sysinit/dune index 04b46fb2a2..f882f987ff 100644 --- a/sysinit/dune +++ b/sysinit/dune @@ -1,7 +1,6 @@ (library (name sysinit) - (public_name coq.sysinit) + (public_name coq-core.sysinit) (synopsis "Coq's initialization") (wrapped false) - (libraries coq.vernac) - ) + (libraries coq-core.vernac)) |