diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-27 11:05:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-27 11:05:09 +0200 |
| commit | 0b218382841f56408558a09bc7de823319ac8772 (patch) | |
| tree | 4b8ca470afc28a66354519819ab644f6dfe51669 /library | |
| parent | a52d06ea16cff00faa7d2f63ad5c1ca0b58e64b4 (diff) | |
| parent | 8042a9078cb8ee8736593356d1a09311c8eeff2f (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'library')
| -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 *) |