Fix --distribution-label erroneously requiring --development.

Reported by @ensra.

diff --git a/configure b/configure
index a9d02ffc449c793bb0c7f1e958f1c580c368d7c2..269d1927f3a91f79e25cbf0dcfc5e50ec836c0da 100755 (executable)
--- a/configure
+++ b/configure
@@ -261,7 +261,7 @@ EOW
 }
 
 # Check that the user actually wants this version.
-if ($version{LABEL} ne 'release') {
+if (defined $version{REAL_LABEL}) {
        print_warning <<'EOW';
 You are building a development version. This contains code which has
 not been tested as heavily and may contain various faults which could seriously

diff --git a/make/common.pm b/make/common.pm
index ba6b03f87d4472d19640e98021c0f3114578cd38..742d372245619a4138dc22119cb7cd521c9cd734 100644 (file)
--- a/make/common.pm
+++ b/make/common.pm
@@ -68,6 +68,7 @@ sub get_version {
 
        # If the user has specified a distribution label then we use it in
        # place of the label from src/version.sh or Git.
+       $version{REAL_LABEL} = $version{LABEL};
        $version{LABEL} = shift // $version{LABEL};
 
        # If any of these fields are missing then the user has deleted the