diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:45:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-27 16:45:03 +0100 |
| commit | 86cada15ad12e31b1f9fe6f0b7026860f45671b4 (patch) | |
| tree | 00815df07b0e6d0e8367b98b2db3a5863129bc69 /vernac/vernacentries.ml | |
| parent | 4774a3129f4175b0b97d538a1c61eb084332fd85 (diff) | |
| parent | f36ea3ffb4ef01572db437392174f10650bee67b (diff) | |
Merge PR #6041: Protecting the printing of filenames with space
Diffstat (limited to 'vernac/vernacentries.ml')
| -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 62c7edb19..6a28d701a 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 = |