Skip to content

Add index page for dev docs #5

Add index page for dev docs

Add index page for dev docs #5

# Automatic generation of developer documentation will be copied
# and checked into the gh-pages branch.
name: Generate MEOS documentation with Doxygen
on:
push:
paths:
- '.github/workflows/generate_dev_docs.yml'
- './meos/**'
- './mobilitydb/**'
- './postgis/**'
- './doxygen/**'
branches:
- master
- develop
- devdocs
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 master
- name: Rename the directory to master
if: ${{ github.ref == 'refs/heads/master' }}
run: |
rm -rf master-dev
mv devdocs-temp master-dev
# Rename the directory to develop
- name: Rename the directory to develop
if: ${{ github.ref == 'refs/heads/develop' }}
run: |
rm -rf develop-dev
mv devdocs-temp develop-dev
# Rename the directory to devdocs
- name: Rename the directory to devdocs
if: ${{ github.ref == 'refs/heads/devdocs' }}
run: |
rm -rf devdocs-dev
mv devdocs-temp devdocs-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