#!/usr/bin/env bash # Copyright 2016-2017 Luke T. 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 unset GIT_INDEX_FILE git worktree add "${gitdir}/pre-generated" pre-generated ( unset GIT_DIR GIT_WORK_TREE cd "$workdir" git merge master -m 'bogus' make --always-make -j12 git add . git commit --amend -m "make: $(git log -n1 master --pretty=format:%B)" ) rm -rf -- "$workdir" git worktree prune fi