diff options
| -rwxr-xr-x | bin/post-commit | 49 |
1 files changed, 31 insertions, 18 deletions
diff --git a/bin/post-commit b/bin/post-commit index 6b72bd2..489181f 100755 --- a/bin/post-commit +++ b/bin/post-commit @@ -1,25 +1,38 @@ #!/usr/bin/env bash +# Copyright 2016-2017 Luke Shumaker +set -e -branch=$(git name-rev --name-only HEAD) -if [[ $branch == master ]]; then +main() { + branch=$(git name-rev --name-only HEAD) + if [[ $branch == master ]]; then + gitdir="$(git rev-parse --git-dir)" + workdir="${gitdir}/pre-generated" + exec 8>"${workdir}.lock" + flock 8 - stash=false - if [[ -n "$(git status --porcelain)" ]]; then - stash=true - git add . - git stash - fi + rm -rf -- "$workdir" + git worktree prune + git branch -D pre-generated.tmp &>/dev/null || true + + git worktree add -b pre-generated.tmp "${gitdir}/pre-generated" master + ( + unset GIT_DIR GIT_WORK_TREE + cd "$workdir" + msg="$(git log -n1 master --pretty=format:%B)" - git checkout pre-generated - git merge master -m 'bogus' - rm -rf out - make --always-make -j12 - git add . - git commit --amend -m "make: $(git log -n1 master --pretty=format:%B)" - git checkout master + make -j1 + echo '!/out/' >> .gitignore - if $stash; then - git stash pop + git add . + git commit -m "make: $msg" + git merge --no-edit -s ours pre-generated + git checkout pre-generated + git merge pre-generated.tmp + git branch -d pre-generated.tmp + ) + rm -rf -- "$workdir" + git worktree prune fi +} -fi +main &>/dev/tty & |