diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-14 11:10:10 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-14 11:10:10 +0200 |
| commit | fb8e41ba16f3d52faabff5737ecdd80eb4715e82 (patch) | |
| tree | 45d6d50d6be0c2d78a9fe2d8b1d560138a358f2d /configure.ml | |
| parent | ff67a511a358ada3daefea0839e18d474531e13d (diff) | |
configure: use ln on linux and cp on windows
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/configure.ml b/configure.ml index f2f239075..71502058f 100644 --- a/configure.ml +++ b/configure.ml @@ -1061,6 +1061,16 @@ 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 *) |