diff options
author | Ben Sima <ben@bsima.me> | 2020-12-28 22:23:52 -0500 |
---|---|---|
committer | Ben Sima <ben@bsima.me> | 2020-12-28 22:33:10 -0500 |
commit | ba9e18d213f7aaf47fa57ccc4d139bc5cfe03d31 (patch) | |
tree | 2f90df7b3be6cd7703d7af33856a5b71fb369b3d /Biz/Ide/post-checkout | |
parent | 9824011e9dfeb46914c60f07ee3634fa9e54ec03 (diff) |
ide: incremental tags and git hooks
Diffstat (limited to 'Biz/Ide/post-checkout')
-rwxr-xr-x | Biz/Ide/post-checkout | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/Biz/Ide/post-checkout b/Biz/Ide/post-checkout new file mode 100755 index 0000000..5474b5a --- /dev/null +++ b/Biz/Ide/post-checkout @@ -0,0 +1,28 @@ +#!/usr/bin/env bash +set -eu + +# Path to wherever you put this. +init_tags=$BIZ_ROOT/Biz/Ide/init_tags.sh + +old=$1 +new=$2 +# is_branch=$2 # 1 if branch, 2 if file + +# filter out only the changed files +changed=($(git diff --name-only $old $new)) + +if [[ ! -r tags ]] +then + $init_tags +elif [[ ${#changed} -gt 0 ]] +then + grep -v -F --regexp=${^changed} $BIZ_ROOT/tags > $BIZ_ROOT/tags.tmp + mv tags.tmp tags + + # Retag all hs files except the ones that were deleted. + modified=($(git diff --name-only --diff-filter=d $old $new)) + # Filter *.hs, since grep returns non-zero for no matches. + modified=(${(M)modified:#*.hs}) + echo "modified: $modified" + $init_tags $modified +fi |