commit fa4b532665ee9cc91570d5cf8bed72e46410a922 parent 0d9eba14dbb11adb56e7bffdb1e20d3a20ce62d8 Author: Oscar Benedito <oscar@oscarbenedito.com> Date: Thu, 6 Jan 2022 18:23:08 +0100 Git user now handles repository mirroring Diffstat:
| A | subscripts/mirror-repository | | | 18 | ++++++++++++++++++ |
| M | subscripts/post-update-public-repos | | | 12 | ++++++------ |
2 files changed, 24 insertions(+), 6 deletions(-)
diff --git a/subscripts/mirror-repository b/subscripts/mirror-repository @@ -0,0 +1,18 @@ +#!/usr/bin/env bash + +set -e + +trap "notify \"ERROR pushing $repo\" \"There was an error pushing $repo to either SourceHut or GitHub.\"" ERR + +dir="$(pwd)" +repo="$(basename "$(pwd)" ".git")" + +git -C "$dir" remote get-url srht || + \ git -C "$dir" remote add srht "git@git.sr.ht:~ob/$repo" +git -C "$dir" push --all --force --prune srht +git -C "$dir" push --tags --force --prune srht + +git -C "$dir" remote get-url github || + \ git -C "$dir" remote add github "git@github.com:oscarbenedito/$repo" +git -C "$dir" push --all --force --prune github +git -C "$dir" push --tags --force --prune github diff --git a/subscripts/post-update-public-repos b/subscripts/post-update-public-repos @@ -1,10 +1,10 @@ #!/bin/sh -# TODO make sure you put the correct token. git update-server-info -dir="$(basename "$(basename "$(pwd)")" ".git")" -curl -X POST -H "Content-Type: application/json" \ - -d "{ \"c\": \"token\", \"r\": \"$dir\" }" \ - "http://localhost:9090/hooks/mirror-repo" \ - >/dev/null 2>/dev/null +# if repository is public, mirror to SourceHut and GitHub +if [ -f "git-daemon-export-ok" ] && [ -f "category" ]; then + # piping into at(1) as a workaround to let git connection finish before + # script has finished running + echo "$(dirname "$(realpath "$0")")/mirror-repository $(pwd)" | at now 2>/dev/null +fi