diff options
| -rw-r--r-- | library/library.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml index e595df092c..da7c4ebb04 100644 --- a/library/library.ml +++ b/library/library.ml @@ -197,8 +197,7 @@ let register_library_filename dir f = LibraryFilenameMap.add dir f !libraries_filename_table let library_full_filename dir = - try LibraryFilenameMap.find dir !libraries_filename_table - with Not_found -> "unavailable" + LibraryFilenameMap.find dir !libraries_filename_table let library_is_loaded dir = try let _ = find_library dir in true |