Add logging of useful DB server information #590

	name: Remove deployment

	on:
	delete:
	pull_request_target:
	types: [ closed ]

	concurrency:
	group: deploy
	cancel-in-progress: false

	jobs:
	main:
	if: github.repository_owner == 'elan-ev'
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v3

	- name: prepare deploy key
	env:
	DEPLOY_KEY: ${{ secrets.DEPLOY_KEY }}
	run: \|
	install -dm 700 ~/.ssh/
	echo "${DEPLOY_KEY}" > ~/.ssh/id_ed25519
	chmod 600 ~/.ssh/id_ed25519
	ssh-keyscan tobira.opencast.org >> ~/.ssh/known_hosts

	- name: install ansible postgres extensions
	run: ansible-galaxy collection install community.postgresql

	- name: Write deploy ID (for branch) to file
	run: echo "DEPLOY_ID=$(./.deployment/deploy-id.sh "${{ github.event.ref }}")" >> $GITHUB_ENV
	if: github.event_name == 'delete'

	- name: Write deploy ID (for PR) to file
	run: echo "DEPLOY_ID=pr${{ github.event.pull_request.number }}" >> $GITHUB_ENV
	if: github.event_name != 'delete'

	- name: Delete GitHub deployment status
	uses: bobheadxi/[email protected]
	with:
	# We would like to `delete-env` instead, but this requires additional
	# permissions for the GITHUB_TOKEN. Fixing that seems to be fairly
	# involved, unfortunately.
	step: deactivate-env
	token: ${{ secrets.GITHUB_TOKEN }}
	env: test-deployment-${{ env.DEPLOY_ID }}

	- name: remove deployment
	working-directory: .deployment
	run: >
	ansible-playbook
	--private-key=~/.ssh/id_ed25519
	--extra-vars="deployid='${{ env.DEPLOY_ID }}'"
	-u github
	remove-deployment.yml

Provide feedback