diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/configure b/configure new file mode 100755 index 00000000..2f4edf34 --- /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 |