From fa475d37fde87683a38f765588aadac22acf6b93 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 28 Aug 2018 15:40:15 +0200
Subject: Remove leftover Makefile.config before configuration

So that if an error occurs during configuration, there is no
Makefile.config file and "make" will fail.

Closes: #244
---
 configure | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/configure b/configure
index 1c1a4c36..c7ccc038 100755
--- a/configure
+++ b/configure
@@ -86,6 +86,10 @@ Options:
   -ignore-coq-version  Accept to use experimental or unsupported versions of Coq
 '
 
+#
+# Remove Leftover Makefile.config (if any)  (GPR#244)
+#
+rm -f Makefile.config
 
 #
 # Parse Command-Line Arguments
-- 
cgit 


From 57b9c642757f6458d4d61a4095b12ab0c0f71dc4 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 28 Aug 2018 15:48:02 +0200
Subject: Improve reporting of configuration errors

The full "usage" text is so long that the actual error message scrolls off
the screen.

With this commit, instead, a short (3-line) error message is printed,
with a suggestion to do `./configure -help`.

The whole "usage" text is printed by `./configure -help`.

Also: better error message for unknown options (arguments starting with `-`).
---
 configure | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/configure b/configure
index c7ccc038..7394091f 100755
--- a/configure
+++ b/configure
@@ -29,6 +29,10 @@ responsefile="gnu"
 ignore_coq_version=false
 
 usage='Usage: ./configure [options] target
+For help on options and targets, do: ./configure -help
+'
+
+help='Usage: ./configure [options] target
 
 Supported targets:
   ppc-eabi             (PowerPC, EABI with GNU/Unix tools)
@@ -119,6 +123,12 @@ while : ; do
         ignore_coq_version=true;;
     -install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev)
         install_coqdev=true;;
+    -help|--help)
+        echo "$help"; exit 0;;
+    -*)
+        echo "Error: unknown option '$1'." 1>&2
+        echo "$usage" 1>&2
+        exit 2;;
     *)
         if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
         target="$1";;
-- 
cgit