From 99e114f5c598ce6321c81bbe41e212877a3c375c Mon Sep 17 00:00:00 2001 From: Ben Sima Date: Mon, 1 Apr 2024 16:35:15 -0400 Subject: Make bild exception for git hooks Apparently git hooks don't get called if they have a file extention, so these weren't getting called at all since commit 904de577261e7024373e7a42fd763184764238f9. So this renames them back to the extension-less versions, and adds an exception in bild for files in the core.hooksPath directory. Unfortunately this means Lint.hs will silently ignore these files, but I guess that's okay for now. --- Biz/Ide/hooks/pre-push | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100755 Biz/Ide/hooks/pre-push (limited to 'Biz/Ide/hooks/pre-push') diff --git a/Biz/Ide/hooks/pre-push b/Biz/Ide/hooks/pre-push new file mode 100755 index 0000000..16f11d1 --- /dev/null +++ b/Biz/Ide/hooks/pre-push @@ -0,0 +1,54 @@ +#!/usr/bin/env bash +# +# A simple ci that saves its results in a git note, formatted according to +# RFC-2822, more or less. +# +# To run this manually, exec the script. It will expect to read a line of +# inputs, you can just enter 'HEAD' and it will +# +## + set -uo pipefail + [[ -n $(git status -s) ]] && { echo fail: dirty worktree; exit 1; } +## + at=$(date -R) + user=$(git config --get user.name) + mail=$(git config --get user.email) +## + commit=$(git notes --ref=ci show HEAD || true) + if [[ -n "$commit" ]] + then + if grep -q "Lint-is: good" <<< "$commit" + then + exit 0 + fi + if grep -q "Test-is: good" <<< "$commit" + then + exit 0 + fi + fi +## + if lint "${CODEROOT:?}"/**/* + then + lint_result="good" + else + lint_result="fail" + exit 1 + fi +## + if bild "${BILD_ARGS:-""}" --test "${CODEROOT:?}"/**/* + then + test_result="good" + else + test_result="fail" + exit 1 + fi +## + read -r -d '' note < +Test-at: $at +EOF +## + git notes --ref=ci append -m "$note" +## -- cgit v1.2.3