Repositories

Create a repository

In Cloud (Repositories → New repository) or the Git portal (your organization → New repository). You need git:write. Names are 3–40 lowercase letters, numbers and dashes, unique in the organization.

Repositories are stored in AWS CodeCommit in the platform's home region, us-west-1, one per repository and named after your organization, so other organizations can't see or reach them.

Clone URL

https://git.dev.superintelligence.gov.vin/<org>/<repo>.git

<org> is your organization's slug. The Git portal's Code button shows the URL with a copy button, and so does the repository list in Cloud.

Authenticate

Git uses HTTP Basic authentication. The username can be anything; the password is a key of your organization:

Any key type works; an API key with just the git scopes is the usual choice. Expired and revoked keys are rejected. Git asks for credentials only after the server challenges it, and a credential helper saves you entering the key each time.

git clone https://git.dev.superintelligence.gov.vin/<org>/<repo>.git
# Username: anything
# Password: the key

A key from another organization is rejected and Git asks for credentials again. A repository that doesn't exist answers 404.

Pushing deploys

Pushing a branch starts a deployment for every project linked to the repository (see The build pipeline). Pushing tags and deleting branches don't deploy.

Limits

• One push request can carry up to about 6 MB. Larger pushes fail; push in smaller pieces, for example a few commits at a time.
• Requests time out after 5 minutes.
• Pushes larger than 6 MB. Coming soon

Delete a repository

In the Git portal, open the repository's Settings → Delete repository and type its full name to confirm (needs git:write). This deletes its branches and history and can't be undone. Its issues and pull requests are no longer shown.