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

---
 configure.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'configure.ml')

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