From 0b069d43bd673341f5f115d21b7bb805d485a5ae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 29 Sep 2017 12:45:17 +0200
Subject: 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.
---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/vernacentries.ml')

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 =
-- 
cgit v1.2.3