src: remote: Fix bug when the user asks to remove IP from known host #363

	name: Test setup and doc build
	on:
	[push, pull_request]
	jobs:
	setup-and-doc-build:
	runs-on: ubuntu-latest
	defaults:
	run:
	shell: bash

	steps:
	- name: Checkout repository
	uses: actions/checkout@v4

	# This is here just because git-email cannot be installed in the
	# Github CI otherwise.
	- name: Add git-core PPA for git-email
	run: \|
	sudo add-apt-repository ppa:git-core/ppa -y

	- name: Update the system
	run: \|
	sudo apt update -y

	- name: Install dependencies
	run: \|
	sudo apt install -y python3-docutils python3-sphinx graphviz

	- name: Check documentation
	run: \|
	./setup.sh --docs --force

	- name: Check installation
	run: \|
	./setup.sh -i --force

Provide feedback