aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-05-08 15:44:02 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-05-08 15:44:02 +0000
commitc5eed70dafdc8a3984d797d0c0349933f808d6bb (patch)
tree8d2aea277a6d890aa99b4ff4d3c647ab8e15fce6 /lib
parent68d0e012b7bce8d48b20bcc1238cad0668063b09 (diff)
un argument booleen inutilisé dans expand_macros
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5737 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/system.ml12
1 files changed, 5 insertions, 7 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 35584bf89..89ff0d2d1 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -32,7 +32,7 @@ let rec expand_atom s i =
then expand_atom s (i+1)
else i
-let rec expand_macros b s i =
+let rec expand_macros s i =
let l = String.length s in
if i=l then s else
match s.[i] with
@@ -40,9 +40,7 @@ let rec expand_macros b s i =
let n = expand_atom s (i+1) in
let v = safe_getenv (String.sub s (i+1) (n-i-1)) in
let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in
- expand_macros false s (i + String.length v)
- | '/' ->
- expand_macros true s (i+1)
+ expand_macros s (i + String.length v)
| '~' ->
let n = expand_atom s (i+1) in
let v =
@@ -50,10 +48,10 @@ let rec expand_macros b s i =
else (getpwnam (String.sub s (i+1) (n-i-1))).pw_dir
in
let s = v^(String.sub s n (l-n)) in
- expand_macros false s (String.length v)
- | c -> expand_macros false s (i+1)
+ expand_macros s (String.length v)
+ | c -> expand_macros s (i+1)
-let glob s = expand_macros true s 0
+let glob s = expand_macros s 0
(* Files and load path. *)