Remove a default repository
Existing workspaces keep their entries.
openapi/harthelm.yaml at v1.5.0__Host-harthelm_session<token>Browser session of the UI (12 h idle, 7 days absolute). State-changing requests also need the header
Harthelm-CSRF: 1 and a matching Origin.
team*integerNumeric resource id.
int641 <= valueprovider*stringProvider id from GET /git/providers.
^[a-z][a-z0-9-]{0,30}$owner*stringOwner (user or organization) of the repository at the provider.
^[A-Za-z0-9][A-Za-z0-9._-]{0,99}$repo*stringRepository name without .git.
^[A-Za-z0-9][A-Za-z0-9._-]{0,99}$Removed.
curl -X DELETE 'https://console.example.com/api/v1/teams/1/git-access/string/string/string'Pull the current branch
`git pull --ff-only` in `/data/app` through the git proxy, as the workspace. It never syncs the landscape. A pull git refuses answers 409 with problem `git-pull-failed` and git's output as `detail`. Needs `workspace.code`; 409 when the IDE does not run.
Revoke a repository
Removes the repository from the workspace's list of repositories the git proxy lets it reach; the next git request for it gets 403. Audited as `git_access.remove`. Needs `workspace.git_access`.