aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/coqinit.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5a262fb1ca..d4257e561a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -93,9 +93,10 @@ let init_load_path () =
(* first, developer specific directory to open *)
if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
(* main loops *)
- Mltop.add_ml_dir (coqlib/"toploop");
- if Coq_config.local then Mltop.add_ml_dir (coqlib/"stm");
- if Coq_config.local then Mltop.add_ml_dir (coqlib/"ide");
+ if Coq_config.local || !Flags.boot then
+ let () = Mltop.add_ml_dir (coqlib/"stm") in
+ Mltop.add_ml_dir (coqlib/"ide")
+ else Mltop.add_ml_dir (coqlib/"toploop");
(* then standard library *)
add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
(* then plugins *)