Allow devdoc action to be run manually (#604) #11

	# Automatic generation of developer documentation will be copied
	# and checked into the gh-pages branch.
	name: Generate MEOS documentation with Doxygen

	on:
	workflow_dispatch:
	push:
	paths:
	- '.github/workflows/generate_dev_docs.yml'
	- './meos/**'
	- './mobilitydb/**'
	- './doxygen/**'
	branches:
	- 'master'
	- 'stable-[0-9]+.[0-9]+'

	jobs:
	build:
	name: Generate MEOS documentation
	runs-on: ubuntu-latest

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

	# generate the documentation files
	- name: Generate documentation
	uses: mattnotmitt/doxygen-action@v1.9.5
	with:
	doxyfile-path: "doxygen/Doxyfile_gha"

	# store the documentation files
	- name: Upload output directory
	uses: actions/upload-artifact@v4
	with:
	name: devdocs-files
	path: \|
	docs/html/*
	retention-days: 1
	copy:
	name: Deploy documentation
	runs-on: ubuntu-latest
	needs: build

	steps:
	# checkout the gh-pages branch
	- uses: actions/checkout@v4
	with:
	ref: gh-pages

	# download the doc files, most of which are generated above
	- name: Download output directory
	uses: actions/download-artifact@v4
	with:
	name: devdocs-files
	path: devdocs-temp

	# Rename the directory to branch name
	- name: Rename the directory to branch name
	run: \|
	rm -rf ${{ github.ref_name }}-dev
	mv devdocs-temp ${{ github.ref_name }}-dev

	# add, commit and push to gh-pages
	- name: Commit changes
	uses: EndBug/add-and-commit@v9
	with:
	message: 'Update dev docs'
	default_author: github_actions

Provide feedback