Delete a push mirror
delete_push_mirrorRemoves a repository's push mirror by remote name, stopping syncs to that remote while leaving the remote repository and already-pushed data untouched.
Instructions
Remove one push mirror from a repository, by its remote_name from list_push_mirrors. Requires write mode. Only the mirror's configuration goes: syncing to that remote stops, and the remote repository and everything already pushed to it are left untouched. Answers {deleted: remote_name}. To stop syncing on every commit but keep the mirror, there is no edit tool; delete it and add it again with add_push_mirror.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| repo | Yes | Repository name. | |
| owner | Yes | Repository owner. | |
| remote_name | Yes | The mirror's `remote_name` (as reported by `list_push_mirrors`). |