diff options
| author |  Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-08-25 16:11:34 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-08-25 16:12:02 +0200 |
| commit | f23e7e7d6f8912ef3ddcc6288cd0f5710a12b99a (patch) | |
| tree | 736eac4420e21366eb8eb04fae1250a43d6ea336 /toplevel/coqinit.ml | |
| parent | 4fef230a1ee1964712e3ac7f325ce00968ac4769 (diff) | |
Prerequisite to fix stm test-suite when not in -local
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 5a262fb1c..d4257e561 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 *) |