diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-02-05 08:04:11 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-02-05 08:04:11 +0100 |
| commit | 6db9f653c4aa133b161e73bf8f93d066e5858b83 (patch) | |
| tree | 811f63bb0cb942f70fc33905ce92c1d07189dcfd /library/loadpath.mli | |
| parent | e07bce3fa05838c4cd826d1b4349604014705208 (diff) | |
Properly set module names in presence of -Q. (Fix for bug #3958)
This is done by adding a fourth type of loadpath, the ones that are
neither implicit nor root, for the subdirectories of a -Q root.
Note: this means that scanning for available directories is no longer done
on the fly for -Q, but once and for all, as with -R.
Diffstat (limited to 'library/loadpath.mli')
| -rw-r--r-- | library/loadpath.mli | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/library/loadpath.mli b/library/loadpath.mli index 62dc5d591..d4029303d 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -15,11 +15,6 @@ open Names *) -type path_type = - | ImplicitPath (** Can be implicitly appended to a logical path. *) - | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *) - | RootPath (** Can only be a prefix of a logical path. *) - type t (** Type of loadpath bindings. *) @@ -35,7 +30,7 @@ val get_load_paths : unit -> t list val get_paths : unit -> CUnix.physical_path list (** Same as [get_load_paths] but only get the physical part. *) -val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit +val add_load_path : CUnix.physical_path -> DirPath.t -> root:bool -> implicit:bool -> unit (** [add_load_path phys type log] adds the binding [phys := log] to the current loadpaths. *) |