grm

git repo manager for self-hosted git servers
git clone git://sink.krj.st/grm
Log | Files | Refs | README | LICENSE

commit 387eb4b0df49bf492e105a93ce230154862a7d44
parent b176903806c5312c35f98a805f4f16b88de3a224
Author: krasjet <nil@krj.st>
Date:   Sun, 12 Jul 2020 16:51:21 -0700

rc: only build index for public repos

Diffstat:
Mgrm | 12+++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/grm b/grm @@ -52,7 +52,17 @@ recompile_repo() { rebuild_index() { echo "[index] rebuilding index..." - stagit-index "${repos_root}/"*.git/ > "${web_root}/index.html" + # 1. find all directories in $repos_root ending with .git + # 2. filter all the public repos (with git-daemon-export-ok) + # 3. run stagit-index on the result + # 4. export result to index.html + find "${repos_root}/." ! -name . -prune \ + -type d -name "*.git" \ + \( \ + -exec test -e "{}/git-daemon-export-ok" \; \ + -o \ + -exec stagit-index {} + \ + \) > "${web_root}/index.html" echo "[index] done!" }