How to add a git repository with a custom ssh port
Please see this guide for adding git repositories to Domino.
If you want to add a repo from a git server with ssh configured to another port (in this example, it's 12345) you will need to use the below format:
If you have any issues setting this up, please let us know!
Note: Don't forget to add your git credentials for the domain in question.