diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-14 19:27:55 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-14 19:28:05 +0200 |
| commit | 01fa046646398890e64d6effbefd1d2a792dff4e (patch) | |
| tree | ea08df9b26ec34f92b13c86e18d9a0928b7fd14e | |
| parent | ee5ea47d525530ea99203211668effc3ae3b30f8 (diff) | |
Fix ML paths (thanks Jean-Marc Notin for bisecting it)
| -rw-r--r-- | toplevel/coqinit.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e95f59f67..0e52fe6ab 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 *) - if Coq_config.local || !Flags.boot then + if Coq_config.local || !Flags.boot then begin let () = Mltop.add_ml_dir (coqlib/"stm") in - Mltop.add_ml_dir (coqlib/"ide"); + Mltop.add_ml_dir (coqlib/"ide") + end; Mltop.add_ml_dir (coqlib/"toploop"); (* then standard library *) add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; |