Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de

chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML
Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ...


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 38ae32912..0278a16cd 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -315,14 +315,14 @@ let parse_file_action reqid file_name =
 		   fnl () ++ Cerrors.explain_exn e));;
 
 let add_rec_path_action reqid string_arg ident_arg =
-  let directory_name = glob string_arg in
+  let directory_name = expand_path_macros string_arg in
     begin
       add_rec_path directory_name (Libnames.dirpath_of_string ident_arg)
     end;;
 	
 
 let add_path_action reqid string_arg =
-  let directory_name = glob string_arg in
+  let directory_name = expand_path_macros string_arg in
     begin
       add_path directory_name Names.empty_dirpath
     end;;