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.sh41
1 files changed, 41 insertions, 0 deletions
diff --git a/Build/source/libs/mpfr/mpfr-src/version-ext.sh b/Build/source/libs/mpfr/mpfr-src/version-ext.sh
new file mode 100644
index 00000000000..936092123cd
--- /dev/null
+++ b/Build/source/libs/mpfr/mpfr-src/version-ext.sh
@@ -0,0 +1,41 @@
+#!/bin/sh
+
+# This script outputs additional MPFR version information for a
+# 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.
+# 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.
+
+set -e
+
+if [ "x`git rev-parse --is-inside-work-tree 2> /dev/null`" != xtrue ]; then
+ echo "$0: This script should be executed from a Git working tree." >&2
+ exit 1
+fi
+
+# Normally passed by tests/Makefile.am with "GREP=$(GREP) SED=$(SED)".
+GREP=${GREP:-grep}
+SED=${SED:-sed}
+
+git tag --contains | $SED -n 's/-root$//p' > excluded-branches
+gitb=`git branch --format='%(refname:short)' --contains | \
+ $SED 's,(HEAD detached at origin/\(.*\)),\1,' | \
+ $GREP -v '^(' | $GREP -v -F -f excluded-branches -x || true`
+rm excluded-branches
+gitc=`git rev-list --count HEAD`
+gith=`git rev-parse --short HEAD`
+gitm=`git update-index -q --refresh; git diff-index --name-only HEAD`
+echo "${gitb:-(none)}-$gitc-$gith${gitm:+ (modified)}"
+
+# References:
+# https://stackoverflow.com/q/3882838/3782797
+# https://stackoverflow.com/a/3899339/3782797
+# for the "git diff-index --name-only HEAD" solution, but this
+# is not sufficient, because autogen.sh modifies the "INSTALL"
+# and "doc/texinfo.tex" files (due to "autoreconf -f -i"), and
+# restores them. On needs:
+# https://stackoverflow.com/q/3882838/3782797#comment121636904_3899339
+# suggesting "git update-index -q --refresh" first.