diff options
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6191f37080..76a3dc8c2c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -153,7 +153,7 @@ let show_match id = let print_path_entry p = let dir = DirPath.print (Loadpath.logical p) in - let path = str (Loadpath.physical p) in + let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in Pp.hov 2 (dir ++ spc () ++ path) let print_loadpath dir = |