diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-29 14:49:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-29 14:51:53 +0100 |
| commit | a4dce1658f9a946cedb40ddcf0cdbc5391dd2005 (patch) | |
| tree | c20ba51c0b1d83466e235c8ef75d337dd59b919b /checker | |
| parent | 8ddc9cbd13ffc22a5895560102852506c9b1ece3 (diff) | |
Forbid implicitly relative names in the checker.
Before this patch, passing a mere identifier (without dots) to the checker
would make it consider it as implicitly referring to a relative name. For
instance, if passed "foo", it would have looked for "Bar.foo.vo" and
"Qux.foo.vo" if those files were in the loadpath.
This was quite ad-hoc. We remove this "feature" and require the user to
always give either a filename or a fully qualified logical name.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/checker/check.ml b/checker/check.ml index 21fdba1fa..a00ec3b0e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -129,8 +129,6 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) -let get_load_paths () = fst !load_paths - (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) @@ -227,13 +225,8 @@ let locate_absolute_library dir = let locate_qualified_library qid = try - let loadpath = - (* Search library in loadpath *) - if qid.dirpath=[] then get_load_paths () - else - (* we assume qid is an absolute dirpath *) - load_paths_of_dir_path (dir_of_path qid) - in + (* we assume qid is an absolute dirpath *) + let loadpath = load_paths_of_dir_path (dir_of_path qid) in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in let path, file = System.where_in_path loadpath name in |