Add ability to mirror from Gitea to GitHub (#30)

This commit is contained in:
Patrick Stevens
2023-04-17 22:49:36 +01:00
committed by GitHub
parent ab88c9db23
commit cd04b1c897
7 changed files with 510 additions and 76 deletions

View File

@@ -7,6 +7,15 @@ open Newtonsoft.Json
type SerialisedMergeStyle = string
[<RequireQualifiedAccess>]
[<Struct>]
[<CLIMutable>]
[<Description "Information about a repo that is to be created on Gitea without syncing from GitHub.">]
type SerialisedPushMirror =
{
GitHubAddress : string
}
[<RequireQualifiedAccess>]
[<Struct>]
[<CLIMutable>]
@@ -55,6 +64,9 @@ type internal SerialisedNativeRepo =
[<JsonProperty(Required = Required.DisallowNull)>]
[<Description "either `true` to allow merging pull requests with a merge commit, or `false` to prevent merging pull requests with merge commits.">]
AllowMergeCommits : Nullable<bool>
[<JsonProperty(Required = Required.DisallowNull)>]
[<Description "Configure a GitHub push mirror to sync this repo to">]
Mirror : Nullable<SerialisedPushMirror>
}
[<Struct>]