aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2001-07-16 14:14:52 +0000
committerfilliatr2001-07-16 14:14:52 +0000
commit4b920ae3c82f857944ea09a22ec74e972a498332 (patch)
treef229facc8f7bca28ab61752a59c80684da3980f1
parent3ffad5af9826ad78c7103ddb23e171667bdd290e (diff)
compat -sort et -suffix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1854 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xtools/coqdep.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 48c6e282e6..272724944b 100755
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -71,10 +71,10 @@ let traite_fichier_ML md ext =
let sort () =
let seen = Hashtbl.create 97 in
let rec loop file =
- let file = file_name file ^ ".v" in
+ let file = file_name file in
if not (Hashtbl.mem seen file) then begin
Hashtbl.add seen file ();
- let cin = open_in file in
+ let cin = open_in (file ^ ".v") in
let lb = Lexing.from_channel cin in
try
while true do
@@ -89,7 +89,7 @@ let sort () =
done
with Fin_fichier ->
close_in cin;
- printf "%s " file
+ printf "%s%s " file !suffixe
end
in
List.iter loop !vAccu