aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-04-17 15:36:11 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-04-17 16:09:47 +0200
commit1c0a1dbfd13f0618b33213c4d42e50d44465c987 (patch)
tree1b268df48a886e63f7848d9b766df43fb69c0d98 /library
parentec462f70ae8062696d4aec8b89c1bb5da3f6a19a (diff)
Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several
libraries at once (see #4193).
Diffstat (limited to 'library')
-rw-r--r--library/library.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index 9d0ccb972..b4261309f 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -633,7 +633,12 @@ let import_module export modl =
with Not_found-> flush acc; safe_locate_module m, [] in
(match m with
| MPfile dir -> aux (dir::acc) l
- | mp -> flush acc; Declaremods.import_module export mp; aux [] l)
+ | mp ->
+ flush acc;
+ try Declaremods.import_module export mp; aux [] l
+ with Not_found ->
+ user_err_loc (loc,"import_library",
+ str ((string_of_qualid dir)^" is not a module")))
| [] -> flush acc
in aux [] modl