Commit 886e2f47 authored by MARCHE Claude's avatar MARCHE Claude

Fix issue #50

share/Makefile.config is created even if enable_relocation
with the relevant info only
parent 48b925c9
......@@ -31,16 +31,19 @@ let localdir = $localdir
let compile_time_support = [ @COMPILETIMECOQ@ @COMPILETIMEPVS@ ]
" > $config
if [ "@enable_relocation@" = "no" ]; then
echo "
BINDIR = $bindir
LIBDIR = $libdir
DATADIR = $datadir
OCAMLBEST = @OCAMLBEST@
BIGINTLIB = @BIGINTLIB@
INCLUDE = @BIGINTINCLUDE@ -I @OCAMLINSTALLLIB@/why3
INCLUDEALL = @BIGINTINCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@ -I @OCAMLINSTALLLIB@/why3
" > $makefileconfig
if [ "@enable_relocation@" = "no" ]; then
echo "
BINDIR = $bindir
LIBDIR = $libdir
DATADIR = $datadir
" >> $makefileconfig
fi
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment