script/install-precommit: work where .git is a file (closes #129)
check / check (push) Successful in 1m19s

The script wrote the hook to .git/hooks, which fails when .git is a
file rather than a directory, as in a clone made with
--separate-git-dir. It now asks git for the repository's own git
directory with `git rev-parse --git-common-dir`, creates its hooks
directory if missing, and writes the hook there. In an ordinary clone
that is .git/hooks, so nothing moves. Before writing anything it stops
with an error when its top directory is not the top of the checkout
git finds, so a copy inside another repository cannot replace that
repository's hook. git's core.hooksPath setting is not followed; where
it is in force, git does not run the installed hook, as before.

Model: opus-5-5
This commit is contained in:
2026-10-01 19:06:34 +00:00
parent f7cc6b42e0
commit 770a68ee02
2 changed files with 16 additions and 1 deletions
+2
View File
@@ -19,6 +19,8 @@ Rationale, Design, TODO, License, Author) if any are still missing.
# Completed Steps
- 2026-10-01: `script/install-precommit` asks git for the repository's git
directory, so `make hooks` also works where `.git` is a file (closes #129).
- 2026-10-01: wildcard CORS now applies only to the public routes, not to
`/metrics`, and allows only the methods they serve (closes #100).
- 2026-10-01: `internal/state` and `internal/watcher` no longer export test-only