aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure
diff options
context:
space:
mode:
authorGravatar mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-22 14:18:38 +0000
committerGravatar mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-22 14:18:38 +0000
commit62ce65dadb0afb8815b26069246832662846c7ec (patch)
tree12d463433d64263510f3875b116f7b8cf16d43bc /configure
parente88df65bbc64b18da34a4233f680829025ca76d9 (diff)
Revert "remove -rectypes except for term.ml"
Preparing landing of the native compiler, which requires -rectypes flag. This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure b/configure
index cb00667ac..c799254ad 100755
--- a/configure
+++ b/configure
@@ -1142,7 +1142,7 @@ CAMLLINK="$bytecamlc"
CAMLOPTLINK="$nativecamlc"
# Caml flags
-CAMLFLAGS=$coq_annotate_flag
+CAMLFLAGS=-rectypes $coq_annotate_flag
TYPEREX=$coq_typerex_wrapper
# Compilation debug flags