aboutsummaryrefslogtreecommitdiff
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 6a913ea894..713b2ad2b6 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -496,9 +496,9 @@ let rec suffixes = function
let add_caml_known phys_dir _ f =
let basename,suff =
- get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in
+ get_extension f [".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] in
match suff with
- | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff
+ | ".ml"|".ml4"|".mlg" -> 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
@@ -584,12 +584,12 @@ let rec treat_file old_dirname old_name =
in
Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
| S_REG ->
- (match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
+ (match get_extension name [".v";".ml";".mli";".ml4";".mlg";".mllib";".mlpack"] with
| (base,".v") ->
let name = file_name base dirname
and absname = absolute_file_name base dirname in
addQueue vAccu (name, absname)
- | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname)
+ | (base,(".ml"|".ml4"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname)
| (base,".mli") -> addQueue mliAccu (base,dirname)
| (base,".mllib") -> addQueue mllibAccu (base,dirname)
| (base,".mlpack") -> addQueue mlpackAccu (base,dirname)