index: add repo url, and search hint #372

	name: build

	on:
	push:
	branches: [master]
	pull_request:
	branches: [master]

	jobs:
	build:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4
	- uses: actions/setup-python@v5
	with:
	python-version: '3.12'
	- name: Install dependencies
	run: \|
	pip3 install -r requirements.txt
	- name: "Linting: autocorrect"
	run: \|
	curl -sSL https://raw.githubusercontent.com/huacnlee/autocorrect/main/install \| sh
	autocorrect --lint
	- name: "Linting: markdownlint"
	uses: DavidAnson/markdownlint-cli2-action@v15
	with:
	globs: docs/*/.md
	- name: Build documentation
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	run: make
	- name: Deploy to GitHub Pages
	if: github.event_name == 'push'
	run: \|
	CINFO="$(git log -1 --pretty="%an: [%h] %B")"
	git clone --depth=1 --branch=gh-pages --single-branch --no-checkout \
	"https://${GITHUB_ACTOR}:${{ secrets.GITHUB_TOKEN }}@github.com/${GITHUB_REPOSITORY}.git" test
	mv test/.git site/.git && rmdir test/
	pushd site/ &>/dev/null
	git add -A
	git -c user.name=GitHub -c [email protected] commit \
	-m "Auto deploy from GitHub Actions build ${GITHUB_RUN_NUMBER}" \
	-m "$CINFO"
	git push
	popd &>/dev/null

Provide feedback