summaryrefslogtreecommitdiff
path: root/Build/source/libs/mpfr/mpfr-src/version-ext.sh
diff options
context:
space:
mode:
Diffstat (limited to 'Build/source/libs/mpfr/mpfr-src/version-ext.sh')
-rw-r--r--Build/source/libs/mpfr/mpfr-src/version-ext.sh12
1 files changed, 11 insertions, 1 deletions
diff --git a/Build/source/libs/mpfr/mpfr-src/version-ext.sh b/Build/source/libs/mpfr/mpfr-src/version-ext.sh
index 936092123cd..9bcc1298907 100644
--- a/Build/source/libs/mpfr/mpfr-src/version-ext.sh
+++ b/Build/source/libs/mpfr/mpfr-src/version-ext.sh
@@ -4,7 +4,8 @@
# Git working tree (Git branch or "(none)", total commit count,
# commit id, and whether the current HEAD is modified). It is
# called in tests/Makefile.am for "make check", but may be used
-# by other tools that need such information.
+# by other tools that need such information (other tests may be
+# needed; see tests/Makefile.am as an example of use).
# Note that this does not replace version information found in
# the VERSION file, which may still need to be output in addition
# to the output of this script.
@@ -20,6 +21,15 @@ fi
GREP=${GREP:-grep}
SED=${SED:-sed}
+# Note: for the branch detection, in the case of a detached HEAD state,
+# the commit may appear in multiple branches, i.e. which diverge after
+# the commit; thus we exclude branches created after this commit, based
+# on <branch>-root tags (such a tag should be added by the user when
+# creating a branch, so that "git diff <branch>-root" shows commits done
+# in the branch since its creation, etc.). If $gitb contains multiple
+# branches, this means that something is probably wrong with the tags
+# or the branches (merged branches should be deleted).
+
git tag --contains | $SED -n 's/-root$//p' > excluded-branches
gitb=`git branch --format='%(refname:short)' --contains | \
$SED 's,(HEAD detached at origin/\(.*\)),\1,' | \