pile

commit 8370db4a3524a1a682c8facdc76576a9d5f26476
parent 80577a8e3ca83db459682bca7a8554ca68dff0af
Author: Kévin Le Gouguec <kevin.legouguec@gmail.com>
Date:   Thu, 18 Jun 2026 18:42:33 +0200

Ponder deep questions

Diffstat:
M
git/post-receive
 | 
4
++++

1 file changed, 4 insertions(+), 0 deletions(-)
diff --git a/git/post-receive b/git/post-receive
@@ -10,6 +10,10 @@ declare -r WWW_REPO_DIR=$(git remote get-url www)
 
 v () {( set -x ; "$@" )}
 
+# TODO: Replace --mirror with refs/heads/* refs/tags/*?
+# --mirror pushes refs/remotes/www/* too, so www records goofy www/*
+# refs that are one push late.
+# (Ideally would use --branches --tags, but seem mutually exclusive)
 v git push --force --mirror www
 
 cd "${WWW_REPO_DIR}"