diff options
Diffstat (limited to 'contrib/interface/parse.ml')
| -rw-r--r-- | contrib/interface/parse.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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;; |