From 4c4aebcb3b28c35b0534329dc43e7e7ff475c97b Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 6 Oct 2016 18:33:04 +0200 Subject: Added configure switch for merlin. The new configure switch generates a .merlin file and adds the -bin-annot flag to the compile options. Bug 20081 --- configure | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/configure b/configure index c15ce3eb..e4b5a169 100755 --- a/configure +++ b/configure @@ -21,6 +21,7 @@ has_runtime_lib=true has_standard_headers=true clightgen=false responsefile="gnu" +merlin=false usage='Usage: ./configure [options] target @@ -65,6 +66,7 @@ Options: -no-runtime-lib Do not compile nor install the runtime support library -no-standard-headers Do not install nor use the standard .h headers -clightgen Also compile the clightgen tool + -merlin Generate .merlin file ' @@ -89,6 +91,8 @@ while : ; do has_standard_headers=false;; -clightgen) clightgen=true;; + -merlin) + merlin=true;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -435,6 +439,32 @@ if $missingtools; then exit 2 fi +if $merlin; then + cat > .merlin <> Makefile.config <> Makefile.config <