ChangeLog

1 files changed, 34 insertions, 0 deletions

diff --git a/bin/pre-generate b/bin/pre-generate
new file mode 100755
index 0000000..bd1c21e
--- /dev/null
+++ b/bin/pre-generate
@@ -0,0 +1,34 @@
+#!/usr/bin/env bash
+# Copyright 2016-2017 Luke Shumaker
+set -e
+
+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
+
+	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)"
+
+		make -j1
+		echo '!/out/' >> .gitignore
+
+		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