diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-10 02:03:08 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-10 11:39:58 +0200 |
| commit | 78c3d736a6a1c74d9bc8317e15895a1a0fbab341 (patch) | |
| tree | 31f7eaad28d8880a4b97656f28501fa9359ba15f /configure.ml | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
[build] Build checker generated files using a make rule.
Currently, `configure.ml` does copy/link some files from `kernel` to
`checker` in an ad-hoc way. Instead, it is preferable to add a copy
rule to make and let it handle the dependencies properly.
This also fixes a dependency bug in Windows, as files wouldn't be
properly refreshed if `configure` was not run each time.
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/configure.ml b/configure.ml index e77310eb7..d4750700b 100644 --- a/configure.ml +++ b/configure.ml @@ -1247,17 +1247,6 @@ let write_configml f = let _ = write_configml "config/coq_config.ml" -(** * Symlinks or copies for the checker *) - -let _ = - let prog, args, prf = - if arch = "win32" then "cp", [], "" - else "ln", ["-s"], "../" in - List.iter (fun file -> - ignore(run "rm" ["-f"; "checker/"^file]); - ignore(run ~fatal:true prog (args @ [prf^"kernel/"^file;"checker/"^file]))) - [ "esubst.ml"; "esubst.mli"; "names.ml"; "names.mli" ] - (** * Build the config/Makefile file *) let write_makefile f = |