Merge remote-tracking branch 'office/main'

This commit is contained in:
Geoffrey Frogeye 2024-01-25 23:55:55 +01:00
commit 59db464987

View file

@ -14,9 +14,10 @@
else
(
cd "${r.path}"
${pkgs.git}/bin/git diff --quiet || echo "Repository is dirty!"
${pkgs.git}/bin/git --no-optional-locks diff --quiet || echo "Repository is dirty!"
${pkgs.git}/bin/git pull || true
${pkgs.git}/bin/git push || true
# Only push if there's something to push. Also prevents from trying to push on repos where we don't have rights.
(${pkgs.git}/bin/git --no-optional-locks status --porcelain -b --ignore-submodules | grep ' \[ahead [0-9]\+\]' && ${pkgs.git}/bin/git push) || true
)
fi
'')