diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/push-repo-mirrors.bash | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/scripts/push-repo-mirrors.bash b/scripts/push-repo-mirrors.bash index 43db9a7..2cdc6a9 100644 --- a/scripts/push-repo-mirrors.bash +++ b/scripts/push-repo-mirrors.bash @@ -2,6 +2,14 @@ # This script pushes the repository mirrors to their respective remote URLs if they are defined in the .gitinfo file. +LOCK_FILE=/var/lock/push-repo-mirrors.lock + +exec 9>"$LOCK_FILE" +if ! flock --nonblock 9; then + echo "Another instance is already running. Exiting." + exit 1 +fi + for repository in /repositories/*; do echo "Processing repository: $(basename "$repository")" |