diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-29 12:45:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-23 19:22:19 +0100 |
| commit | 0b069d43bd673341f5f115d21b7bb805d485a5ae (patch) | |
| tree | 1caf03c1257bcaf9f4b54e24e2759ee910a5de62 /vernac | |
| parent | 23f49985296a3594c2cf37fa08e0b3e882d5c9e4 (diff) | |
Quote file names which have spaces in "Print LoadPath".
The primary concern is for clarity of reading.
May it affects tools which would parse the output of "Print LoadPath"?
Presumably, these tools would not support file names with spaces
already, so this may have no impact.
Diffstat (limited to 'vernac')
| -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 6191f3708..76a3dc8c2 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 = |