Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 3 insertions, 3 deletions

diff --git a/configure b/configure
index 9c3d6a7..5a1b4ba 100755
--- a/configure
+++ b/configure
@@ -61,7 +61,7 @@ done
 # Per-target configuration
 
 cchecklink=false
-has_runtime_lib=false
+has_runtime_lib=true
 
 case "$target" in
   powerpc-linux|ppc-linux|powerpc-eabi|ppc-eabi)
@@ -218,8 +218,8 @@ CLINKER=gcc
 # Math library.  Set to empty under MacOS X
 LIBMATH=-lm
 
-# Obsolete; do not change
-HAS_RUNTIME_LIB=false
+# Do not change
+HAS_RUNTIME_LIB=true
 EOF
 fi