For the complete documentation index, see llms.txt. This page is also available as Markdown.

Git Management

The environment source code is hosted on GitHub. Here you can grant and remove access to the repo.

Add Git User

Before you can access your GitHub repository you must add a GitHub user.

Owner, Admin and Developer member roles can add git users.

  1. Click + Add User.

  1. Enter the GitHub username.

  2. Select the appropriate permission level.

  3. Click Add User.

Note the git user permissions:

  • Read can pull source code from repository

  • Write can pull and push changes to repository

  • Triage can pull source code from repository and manage pull requests and issues

Learn more here.

Change Git User permission

Owner, Admin and Developer member roles can change git user permission.

  1. Click the permission dropdown

  1. Select the desired permission level.

  1. The permission is updated automatically upon selection.

Delete User

Should you wish to remove users from your repository you can use the Delete button next to each of the usernames, to delete a specific user.

Last updated