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 `-`).

1 files changed, 10 insertions, 0 deletions

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";;