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

---
 checker/esubst.ml  | 1 -
 checker/esubst.mli | 1 -
 checker/names.ml   | 1 -
 checker/names.mli  | 1 -
 4 files changed, 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

(limited to 'checker')

diff --git a/checker/esubst.ml b/checker/esubst.ml
deleted file mode 120000
index b82bd24f1e..0000000000
--- 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 e30eaae5d3..0000000000
--- 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 f0bf2f83f6..0000000000
--- 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 10459f3b29..0000000000
--- a/checker/names.mli
+++ /dev/null
@@ -1 +0,0 @@
-../kernel/names.mli
\ No newline at end of file
-- 
cgit v1.2.3