diff options
| -rw-r--r-- | lib/system.ml | 2 | ||||
| -rw-r--r-- | vernac/mltop.ml | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml index 12eacf2ea..0b64b237d 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -52,7 +52,7 @@ let dirmap = ref StrMap.empty let make_dir_table dir = let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in - Array.fold_left filter_dotfiles StrSet.empty (readdir dir) + Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) let exists_in_dir_respecting_case dir bf = let cache_dir dir = diff --git a/vernac/mltop.ml b/vernac/mltop.ml index e8a0ba3dd..8ec85688c 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -175,6 +175,7 @@ let warn_cannot_use_directory = let convert_string d = try Names.Id.of_string d with UserError _ -> + let d = Unicode.escaped_if_non_utf8 d in warn_cannot_use_directory d; raise Exit |