diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-31 23:20:21 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 00:53:09 +0200 |
| commit | 1532e4d57fce07e8a1cd6838853a4a31ea84e453 (patch) | |
| tree | a1c3e1f1ca8b5924f60e3756a1f81a6ae8764c7e /tools/coqdep_common.ml | |
| parent | b3485ddc8c4f98743426bb58c8d49b76edd43d61 (diff) | |
Makefile: restore the use of coqdep_boot for creating .v.d files
Coqdep_boot has almost no dependencies, and hence can be compiled
very early during the build, without relying on .ml.d files.
Some code of system.ml is now in a separate file minisys.ml,
which is also included in system.ml for compatibility.
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index c63e4aaa6..0f7937d72 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -9,11 +9,11 @@ open Printf open Coqdep_lexer open Unix -open System +open Minisys (** [coqdep_boot] is a stripped-down version of [coqdep], whose behavior is the one of [coqdep -boot]. Its only dependencies - are [Coqdep_lexer] and [Unix], and it should stay so. + are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via options (see for instance [option_natdynlk] below). *) @@ -526,7 +526,7 @@ let rec add_directory recur add_file phys_dir log_dir = | FileRegular f -> add_file phys_dir log_dir f in - System.check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; + check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; if exists_dir phys_dir then process_directory f phys_dir else |