Use custom SSH port for Github Actions #3

	name: CI/CD
	on:
	push:
	branches:
	- main
	jobs:
	main:
	name: Update PPI repository on trinity after push to main
	runs-on: ubuntu-latest
	steps:
	- name: Execute remote ssh commands using ssh key
	uses: appleboy/[email protected]
	with:
	host: trinity.fsi.uni-tuebingen.de
	username: ${{ secrets.SSH_USERNAME }}
	key: ${{ secrets.SSH_KEY }}
	port: ${{ secrets.SSH_PORT }}
	# stored in secrets because it's easier to change this instead of updating this script
	# i.e. when switching from RSA host key to ED25519
	fingerprint: ${{ secrets.SSH_FINGERPRINT }}
	script: sudo -u www-data /usr/bin/git -C /srv/data/ppi/code/ pull origin main

Provide feedback