aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:01 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:01 +0000
commit59c9403ceb09a35ed219b522e9f5abdb50615d76 (patch)
treef7d3e521f6a948defdce70e00c718c6bdc7b696e /configure
parent1b9428c4e4ce6f2dbe98d0f753b062ae8634a954 (diff)
lib directory is cut in 2 cma.
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure5
1 files changed, 3 insertions, 2 deletions
diff --git a/configure b/configure
index 0fe91b9dc..00938f40f 100755
--- a/configure
+++ b/configure
@@ -1008,6 +1008,7 @@ fi
##############################################
mlconfig_file="$COQSRC/config/coq_config.ml"
+mymlconfig_file="$COQSRC/myocamlbuild_config.ml"
config_file="$COQSRC/config/Makefile"
config_template="$COQSRC/config/Makefile.template"
@@ -1065,7 +1066,7 @@ esac
# Building the $COQTOP/config/coq_config.ml file
#####################################################
-rm -f "$mlconfig_file"
+rm -f "$mlconfig_file" "$mymlconfig_file"
cat << END_OF_COQ_CONFIG > $mlconfig_file
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
@@ -1132,7 +1133,7 @@ subdirs plugins
echo "]" >> "$mlconfig_file"
chmod a-w "$mlconfig_file"
-
+ln -sf "$mlconfig_file" "$mymlconfig_file"
###############################################
# Building the $COQTOP/config/Makefile file