aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-02 01:22:41 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-08 14:32:56 +0200
commit1d6d0060330197896748739a625d0b1c7f083da2 (patch)
tree27da3d5329a91fc262f52e887ee31fa0c37c20e3 /configure.ml
parent2e79ed74824db4697ab1807b6210b3d4097c9fda (diff)
Officially discontinue the experimental coq build via ocamlbuild
It has been accidentaly broken since early 2014 (and especially in 8.5), no easy repair, I won't devote any more hours to this stuff. Moreover no one seems to care apart from Emilio, but he's ok to work on this in a separate repository or branch. I left a dev/doc/ocamlbuild.txt file with a few words about this experiment.
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml11
1 files changed, 2 insertions, 9 deletions
diff --git a/configure.ml b/configure.ml
index ade43810b..1ea56d3ce 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1003,7 +1003,7 @@ let write_dbg_wrapper f =
let _ = write_dbg_wrapper "dev/ocamldebug-coq"
-(** * Build the config/coq_config.ml file (+ link to myocamlbuild_config.ml) *)
+(** * Build the config/coq_config.ml file *)
let write_configml f =
safe_remove f;
@@ -1070,14 +1070,7 @@ let write_configml f =
close_out o;
Unix.chmod f 0o444
-let write_configml_my f f' =
- write_configml f;
- if os_type_win32 then
- write_configml f'
- else
- (safe_remove f'; Unix.symlink f f')
-
-let _ = write_configml_my "config/coq_config.ml" "myocamlbuild_config.ml"
+let _ = write_configml "config/coq_config.ml"
(** * Build the config/Makefile file *)