diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-25 23:38:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-25 23:41:48 +0200 |
| commit | 2fa1dc39371b8f770ce662d56d85bf6f20413aac (patch) | |
| tree | cb4686f5ffad055aff805170ff7d6a059a717498 /library/loadpath.ml | |
| parent | 1ea09cb57dffd7cc9b6fa3ccec137ea3dfcc6980 (diff) | |
Fix bug #5090: Effect of -Q depends on coqtop's current directory.
This bug was seemingly introduced on purpose by commit 9c5ea63 in 2001. It
seems that the original motivation was to deactivate a warning when overriding
the default loadpath binding of the current directory, but in the end it made
it non-overridable.
Diffstat (limited to 'library/loadpath.ml')
| -rw-r--r-- | library/loadpath.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml index e6f6716c3..d03c6c555 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -72,9 +72,6 @@ let add_load_path phys_path coq_path ~implicit = let replace = if DirPath.equal coq_path old_path then implicit <> old_implicit - else if DirPath.equal coq_path (Nameops.default_root_prefix) - && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then - false (* This is the default "-I ." path, don't override the old path *) else let () = (* Do not warn when overriding the default "-I ." path *) |