diff options
| -rw-r--r-- | .gitignore | 4 | ||||
| l--------- | checker/esubst.ml | 1 | ||||
| l--------- | checker/esubst.mli | 1 | ||||
| l--------- | checker/names.ml | 1 | ||||
| l--------- | checker/names.mli | 1 | ||||
| -rw-r--r-- | configure.ml | 10 |
6 files changed, 14 insertions, 4 deletions
diff --git a/.gitignore b/.gitignore index 0193c9dfa..56e190598 100644 --- a/.gitignore +++ b/.gitignore @@ -138,6 +138,10 @@ tools/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt lia.cache +checker/names.ml +checker/names.mli +checker/esubst.ml +checker/esubst.mli # mlis documentation diff --git a/checker/esubst.ml b/checker/esubst.ml deleted file mode 120000 index b82bd24f1..000000000 --- a/checker/esubst.ml +++ /dev/null @@ -1 +0,0 @@ -../kernel/esubst.ml
\ No newline at end of file diff --git a/checker/esubst.mli b/checker/esubst.mli deleted file mode 120000 index e30eaae5d..000000000 --- a/checker/esubst.mli +++ /dev/null @@ -1 +0,0 @@ -../kernel/esubst.mli
\ No newline at end of file diff --git a/checker/names.ml b/checker/names.ml deleted file mode 120000 index f0bf2f83f..000000000 --- a/checker/names.ml +++ /dev/null @@ -1 +0,0 @@ -../kernel/names.ml
\ No newline at end of file diff --git a/checker/names.mli b/checker/names.mli deleted file mode 120000 index 10459f3b2..000000000 --- a/checker/names.mli +++ /dev/null @@ -1 +0,0 @@ -../kernel/names.mli
\ No newline at end of file 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 *) |