Updated expected redirections. (#265) #244

	name: Update GitHub Pages

	on:
	push:
	branches:
	- '[0-9]+.[0-9]+.[0-9]+'
	- '[0-9]+.[0-9]+.[0-9]+-*'
	- update_pages
	- fix-github-workflow

	jobs:

	build:
	runs-on: ubuntu-latest

	steps:
	- uses: actions/checkout@v4

	- name: Setup git identity
	run: \|
	git config --global user.email "emmo.github.action@github.com"
	git config --global user.name "EMMO GitHub Action"

	- name: Setup Python 3.11
	uses: actions/setup-python@v5
	with:
	python-version: 3.11

	- name: Debug info
	run: \|
	echo "GITHUB_REF_NAME=${GITHUB_REF_NAME}"

	- name: Install EMMO-python
	run: \|
	pip install --upgrade pip
	pip install EMMOntoPy

	- name: Install pandoc 2.1.2
	run: \|
	#sudo apt-get install pandoc # we need v2.1.2
	wget https://github.com/jgm/pandoc/releases/download/2.1.2/pandoc-2.1.2-1-amd64.deb
	sudo apt-get install ./pandoc-2.1.2-1-amd64.deb

	- name: Install other dependencies
	run: \|
	sudo apt-get install graphviz
	sudo apt-get install texlive-xetex
	sudo apt-get install texlive-latex-extra
	pip install semver

	- name: Checkout GitHub Pages for EMMO-repo
	uses: actions/checkout@v4
	with:
	repository: emmo-repo/emmo-repo.github.io
	path: ".github/pages"
	ssh-key: ${{ secrets.SSH_PRIVATE_KEY }}
	ssh-strict: no

	- name: Update GitHub Pages
	run: \|
	.github/scripts/update_pages.sh -v -V ${GITHUB_REF_NAME}

Provide feedback