summaryrefslogtreecommitdiff
path: root/.depend
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2022-04-06 15:34:00 +0100
committerDavid Allsopp <david.allsopp@metastack.com>2022-05-24 14:10:09 +0100
commit7c8d877ee4b3875e6316be53dbbcf4f04503c1a1 (patch)
tree9ff8d7bc998eeec55d6abf112603a85d80cda854 /.depend
parent2986a94fa2603db5cca748d1bdbc7edae98c46d7 (diff)
downloadocaml-7c8d877ee4b3875e6316be53dbbcf4f04503c1a1.tar.gz
Add a hook for misses in Load_path
Load_path.find{,_uncap} now invoke a hook before raising Not_found, which provides a mechanism for automatically adding directories to the Load_path if required.
Diffstat (limited to '.depend')
-rw-r--r--.depend1
1 files changed, 1 insertions, 0 deletions
diff --git a/.depend b/.depend
index 79d4c29b02..57789239b9 100644
--- a/.depend
+++ b/.depend
@@ -6019,6 +6019,7 @@ driver/compmisc.cmx : \
utils/clflags.cmx \
driver/compmisc.cmi
driver/compmisc.cmi : \
+ utils/load_path.cmi \
typing/env.cmi \
utils/clflags.cmi
driver/errors.cmo : \