diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/make_git_revision.sh | 11 | ||||
| -rwxr-xr-x | dev/tools/update-compat.py | 2 |
2 files changed, 12 insertions, 1 deletions
diff --git a/dev/tools/make_git_revision.sh b/dev/tools/make_git_revision.sh new file mode 100755 index 0000000000..84982f89b9 --- /dev/null +++ b/dev/tools/make_git_revision.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +if [ -x `which git` ] && [ -d .git ] || git rev-parse --git-dir > /dev/null 2>&1 +then + export LANG=C + GIT_BRANCH=$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p') + GIT_HOST=$(hostname) + GIT_PATH=$(pwd) + echo "${GIT_HOST}:${GIT_PATH},${GIT_BRANCH}" + echo $(git log -1 --pretty='format:%H') +fi diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 7c8b9f025c..14094553a2 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -17,7 +17,7 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') -BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', '4798.v') +BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v')) TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current') |