diff options
| author | Pierre-Marie Pédrot | 2018-10-18 13:40:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 16:19:45 +0200 |
| commit | 3f6eebb9cfeda531d1f71e2ea0fa2d5afa9c28fc (patch) | |
| tree | e714c433208c071b17838f911d74a328b72c636c /tools/coqdep_common.ml | |
| parent | 3799939088b5aa616974a0d37de7e2616024f222 (diff) | |
Adapt coq_makefile to handle coqpp-based macro files.
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 8 |
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) |