diff options
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml index 44e8286ce..2a495f0cf 100644 --- a/library/library.ml +++ b/library/library.ml @@ -144,7 +144,7 @@ let open_library export explicit_libs m = (* Only libraries indirectly to open are not reopen *) (* Libraries explicitly mentionned by the user are always reopen *) List.exists (eq_lib_name m) explicit_libs - or not (library_is_opened m.library_name) + || not (library_is_opened m.library_name) then begin register_open_library export m; Declaremods.really_import_module (MPfile m.library_name) |