diff options
| -rwxr-xr-x | contrib/devtools/github-merge.py | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/devtools/github-merge.py b/contrib/devtools/github-merge.py index 6712d4f3b6..bbebd11e8e 100755 --- a/contrib/devtools/github-merge.py +++ b/contrib/devtools/github-merge.py @@ -168,7 +168,10 @@ def main(): print("git config --global user.signingkey <key>",file=stderr) sys.exit(1) - host_repo = host+":"+repo # shortcut for push/pull target + if host.startswith(('https:','http:')): + host_repo = host+"/"+repo+".git" + else: + host_repo = host+":"+repo # Extract settings from command line args = parse_arguments() |