aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/check.ml')
-rw-r--r--checker/check.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 6f01107f5..3194b2681 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -54,7 +54,7 @@ type library_disk = {
type library_t = {
library_name : compilation_unit_name;
- library_filename : System.physical_path;
+ library_filename : CUnix.physical_path;
library_compiled : Safe_typing.compiled_library;
library_deps : (compilation_unit_name * Digest.t) list;
library_digest : Digest.t }
@@ -114,7 +114,7 @@ let check_one_lib admit (dir,m) =
type logical_path = dir_path
-let load_paths = ref ([],[] : System.physical_path list * logical_path list)
+let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
let get_load_paths () = fst !load_paths