summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-03 10:25:25 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-03 10:25:25 +0000
commit93d89c2b5e8497365be152fb53cb6cd4c5764d34 (patch)
tree0de8d05bbd0eeaeb5e4b85395f8dd576984b6a9e /configure
parent891377ce1962cdb31357d6580d6546ec22df2b4f (diff)
Getting rid of CIL
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure8
1 files changed, 0 insertions, 8 deletions
diff --git a/configure b/configure
index 2b53b44..d8c63fe 100755
--- a/configure
+++ b/configure
@@ -163,14 +163,6 @@ LIBMATH=-lm
EOF
fi
-# Extract and configure Cil
-
-(cd cil && ./configure)
-
-# Extract 'ARCHOS' info from Cil configuration
-
-grep '^ARCHOS=' cil/config.log >> Makefile.config
-
# Summarize configuration
if test "$target" = "manual"; then