Sync: may ignore repositories

diff --git a/share/hydra/sync b/share/hydra/sync
index d425d90c058d3b7d06ede5a891d08242fd9a8073..9b1d0971bd03323bb539662895708df226850ecc 100755 (executable)
--- a/share/hydra/sync
+++ b/share/hydra/sync
@@ -21,6 +21,10 @@ hydra_config_load
 # Sync each repository.
 function hydra_sync {
   for repository in $*; do
+    if [ -e "$HYDRA_FOLDER/config/repository/ignore/$repository" ]; then
+      continue
+    fi
+
     if [ "$repository" == "keyringer" ]; then
       UPDATE_KEYRINGER="yes"
       continue