diff options
Diffstat (limited to 'Build/source/libs/mpfr/mpfr-src/version-ext.sh')
-rw-r--r-- | Build/source/libs/mpfr/mpfr-src/version-ext.sh | 12 |
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,' | \ |