aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-02-06 14:43:15 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-02-06 14:43:15 +0100
commit54fa98c3833091a75d0c1afe84b42afc35452fe3 (patch)
treeda9ecf36e998d99113458852a9d9c6ca33f765e1
parent5920d4c569337b0eb09132f6160d11b9c0c73888 (diff)
downloadcompcert-kvx-54fa98c3833091a75d0c1afe84b42afc35452fe3.tar.gz
compcert-kvx-54fa98c3833091a75d0c1afe84b42afc35452fe3.zip
Removed superfluous check.
-rwxr-xr-xconfigure4
1 files changed, 0 insertions, 4 deletions
diff --git a/configure b/configure
index cda75975..081ac202 100755
--- a/configure
+++ b/configure
@@ -626,12 +626,8 @@ MANDIR=$sharedir/man
SHAREDIR=$sharedir
OCAML_OPT_COMP=$ocaml_opt_comp
MENHIR_INCLUDES=$menhir_includes
-EOF
-if $merlin; then
- cat >> Makefile.config <<EOF
COMPFLAGS=-bin-annot
EOF
-fi
if test "$target" != "manual"; then
cat >> Makefile.config <<EOF