aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/loadpath.mli
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-05-22 10:48:11 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-05-22 10:48:11 +0200
commit4d6a5677f0f4af0193bb42f5d2938287efaaf91b (patch)
treedf73ba2913e000fd809a7ae81e4b6cd82926a765 /library/loadpath.mli
parentcc63a961f846e6e00f56d4c1e98d80fafbfb17b8 (diff)
Fix native_compute for systems with a limited size for the command line.
The call to the native compiler can fail due to the sheer amounts of -I options passed to it. Indeed, it is easy to get the command line to exceed 512KB, thus causing various operating systems to reject it. This commit avoids the issue by only passing the -I options that matter for the currently compiled code. Note that, in the worst case, this commit is still not sufficient on Windows (32KB max), but this worst case should be rather uncommon and thus can be ignored for now. For the record, the command-line size mandated by Posix is 4KB.
Diffstat (limited to 'library/loadpath.mli')
-rw-r--r--library/loadpath.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/library/loadpath.mli b/library/loadpath.mli
index af86122cf..c8bfd2e59 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -35,9 +35,6 @@ 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 get_accessible_paths : unit -> CUnix.physical_path list
-(** Same as [get_paths] but also get paths that can be relatively accessed. *)
-
val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit
(** [add_load_path phys type log] adds the binding [phys := log] to the current
loadpaths. *)