publish.yaml

name: Publish HTML pages

on:
  push:
    branches: [master]
  pull_request:
    types: [opened, reopened, synchronize, labeled]
  workflow_dispatch:

jobs:
  publish-doc:
    if: |
      github.event_name == 'push' ||
      github.event_name == 'pull_request' &&
      github.event.pull_request.head.repo.full_name != github.repository

    runs-on: ubuntu-latest
    steps:
      - uses: tarantool/actions/cleanup@master
      - uses: actions/checkout@v3
        with:
          fetch-depth: 0

      - name: Setup mandoc
        run: sudo apt install -y mandoc

      - name: Build HTML pages
        run: make html

      - name: Publish HTML table of contents
        run: cp index.html man3/

      - name: Publish CSS
        run: cp style.css man3/

      - name: Publish HTML pages to GitHub Pages
        uses: JamesIves/github-pages-deploy-action@v4.4.0
        with:
          folder: man3/
        if: github.ref == 'refs/heads/master' &&
            github.event_name != 'pull_request'