From fb8e41ba16f3d52faabff5737ecdd80eb4715e82 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 14 Jun 2016 11:10:10 +0200
Subject: configure: use ln on linux and cp on windows

---
 .gitignore         |  4 ++++
 checker/esubst.ml  |  1 -
 checker/esubst.mli |  1 -
 checker/names.ml   |  1 -
 checker/names.mli  |  1 -
 configure.ml       | 10 ++++++++++
 6 files changed, 14 insertions(+), 4 deletions(-)
 delete mode 120000 checker/esubst.ml
 delete mode 120000 checker/esubst.mli
 delete mode 120000 checker/names.ml
 delete mode 120000 checker/names.mli

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 *)
 
-- 
cgit v1.2.3