summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xbin/post-commit49
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 &