aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-09-30 13:10:26 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2014-09-30 13:10:26 +0200
commita2bed030e01bfe6e3addbe44f724de5c5fbeab65 (patch)
treeaeffd4bcba1743dd5fdcc08e2f2e9f51962e4402 /configure
parente5b59af8a21c42b504b1beeb89208dd0cb0c8b3b (diff)
downloadcompcert-a2bed030e01bfe6e3addbe44f724de5c5fbeab65.tar.gz
compcert-a2bed030e01bfe6e3addbe44f724de5c5fbeab65.zip
Change the way the tools like the linker, assembler, etc. are specified by including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure3
1 files changed, 3 insertions, 0 deletions
diff --git a/configure b/configure
index 787bd905..fda59dab 100755
--- a/configure
+++ b/configure
@@ -274,11 +274,14 @@ fi
# Generate Makefile.config
+sharedir="$(dirname "$bindir")"/share
+
rm -f Makefile.config
cat > Makefile.config <<EOF
PREFIX=$prefix
BINDIR=$bindir
LIBDIR=$libdir
+SHAREDIR=$sharedir
EOF
if test "$target" != "manual"; then