Remove remote editing from the Git sidebar

This commit is contained in:
2026-07-23 09:38:40 +02:00
parent 08a5bd192c
commit 632822fe1b
13 changed files with 46 additions and 83 deletions

View File

@@ -87,7 +87,6 @@ surface GitControlSurface {
GitHistoryRequested(project, branch)
GitFileHistoryRequested(project, file_path)
GitRemoteStateRequested(project)
GitRemoteSetRequested(project, remote_url)
GitFetchRequested(project)
GitPullRequested(project)
GitPushRequested(project)
@@ -153,12 +152,6 @@ rule GetRemoteState {
ensures: GitRemoteStateReport(project, local_branch, upstream_branch, ahead, behind)
}
rule SetRemote {
when: GitRemoteSetRequested(project, remote_url)
-- Creates origin when absent and replaces its URL when already configured.
ensures: GitRemoteUpdated(project, remote_url)
}
rule Fetch {
when: GitFetchRequested(project)
ensures: RemoteRefsUpdated(project)