aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-29 12:45:17 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-23 19:22:19 +0100
commit0b069d43bd673341f5f115d21b7bb805d485a5ae (patch)
tree1caf03c1257bcaf9f4b54e24e2759ee910a5de62 /vernac
parent23f49985296a3594c2cf37fa08e0b3e882d5c9e4 (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.ml2
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 =