#/bin/bash

# This script is responsible for pushing to mirrors of the git repositories. It runs through all the repositories in the /repositories directory and performs a git push to the corresponding mirror URL(s) defined in the .gitinfo file if they exist.

echo "to be implemented"