diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-24 23:33:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-25 01:19:29 +0200 |
| commit | 1ea09cb57dffd7cc9b6fa3ccec137ea3dfcc6980 (patch) | |
| tree | 37b96a632404da3eadc24b744c19019b75ccb4a2 | |
| parent | f487472a5628fdb43245e782b304705172a1f569 (diff) | |
The coqtop options -Q and -R do not affect the ML loadpath anymore.
It seems that such options were adding the considered path to the ML loadpath
as well, which is not what is documented, and does not provide an atomic way
to manipulate Coq loadpaths.
| -rw-r--r-- | toplevel/coqinit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 8a8dbe960..acbf909cc 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -108,7 +108,7 @@ let init_load_path () = (* additional loadpath, given with options -Q and -R *) List.iter (fun (unix_path, coq_root, implicit) -> - Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit) + Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit) (List.rev !includes); (* additional ml directories, given with option -I *) List.iter Mltop.add_ml_dir (List.rev !ml_includes) |