Michael Hoennig b33bafb753 git-pull-and-run-if-origin-changed: pull every 10s and show commit-ids		2024-09-13 13:57:39 +02:00
..
git-pull-and-if-origin-changed-run-tests	git-pull-and-run-if-origin-changed: pull every 10s and show commit-ids	2024-09-13 13:57:39 +02:00