From dd16448f54b3a7d754b7e511e08b992d3fefc27e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Nov 2006 21:51:18 +0000
Subject: 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
---
 contrib/interface/parse.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/interface/parse.ml')

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 38ae329125..0278a16cd5 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;;
-- 
cgit v1.2.3