summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-08-06 08:45:25 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-08-06 08:45:25 +0000
commit94aea0609bb54f0fde29a558366b646b3b8d21a2 (patch)
tree2c81bb38c04b6ca50dd8588681fe68baa71a237a /configure
parentc0bc146622528e3d52534909f5ae5cd2e375da8f (diff)
Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure42
1 files changed, 42 insertions, 0 deletions
diff --git a/configure b/configure
new file mode 100755
index 0000000..2f4edf3
--- /dev/null
+++ b/configure
@@ -0,0 +1,42 @@
+#!/bin/sh
+
+cildistrib=cil-1.3.5.tar.gz
+prefix=/usr/local
+bindir='$(PREFIX)/bin'
+libdir='$(PREFIX)/lib/compcert'
+
+# Parse command-line arguments
+
+while : ; do
+ case "$1" in
+ "") break;;
+ -prefix|--prefix)
+ prefix=$2; shift;;
+ -bindir|--bindir)
+ bindir=$2; shift;;
+ -libdir|--libdir)
+ libdir=$2; shift;;
+ *) echo "Unknown option \"$1\"." 1>&2; exit 2;;
+ esac
+ shift
+done
+
+# Generate Makefile.config
+
+rm -f Makefile.config
+cat > Makefile.config <<EOF
+PREFIX=$prefix
+BINDIR=$bindir
+LIBDIR=$libdir
+EOF
+
+# Extract and configure Cil
+
+set -e
+tar xzf $cildistrib
+for i in cil.patch/*; do patch -p1 < $i; done
+(cd cil && ./configure)
+
+# Extract 'ARCHOS' info from Cil configuration
+
+grep '^ARCHOS=' cil/config.log >> Makefile.config