diff options
| -rw-r--r-- | git-tools/setup_github_network.php | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/git-tools/setup_github_network.php b/git-tools/setup_github_network.php index 911d336c2d..08e99e2f32 100644 --- a/git-tools/setup_github_network.php +++ b/git-tools/setup_github_network.php @@ -84,6 +84,12 @@ else clone_repository($username, $repository, isset($collaborators[$developer])); } +// Add private security repository for developers +if ($username == 'phpbb' && $repository == 'phpbb3' && isset($collaborators[$developer])) +{ + run("git remote add $username-security " . get_repository_url($username, "$repository-security", true)); +} + // Skip blessed repository. unset($remotes[$username]); |