summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPeter Powell <petpow@saberuk.com>2019-05-03 15:17:15 +0100
committerPeter Powell <petpow@saberuk.com>2019-05-03 15:17:15 +0100
commit044fa999680888267e07dc7b69028b18efbac818 (patch)
treed17eac0a8303611a4461fddad75f784134624d30
parent68e5d0a151d8b5ca6577a0053dcda95774bf323a (diff)
Fix --distribution-label erroneously requiring --development.
Reported by @ensra.
-rwxr-xr-xconfigure2
-rw-r--r--make/common.pm1
2 files changed, 2 insertions, 1 deletions
diff --git a/configure b/configure
index a9d02ffc4..269d1927f 100755
--- 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 ba6b03f87..742d37224 100644
--- 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