From 9aa4b2991d79697b3ad89d70d7af88628bdd46da Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 12 Jan 2015 09:40:58 +0100 Subject: Fixing typo in previous commit. --- tools/coqdep_common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools/coqdep_common.ml') diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index fa6a0daeb..62cfc374a 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -443,7 +443,7 @@ let add_caml_known phys_dir _ f = let basename,suff = get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in match suff with - | ".ml"|".ml4" -> add_ml_known f (Some phys_dir) suff + | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff -- cgit v1.2.3