master.yaml

# a workflow to create the index.html page and related resources and put it for hosting on github_pages.

name: Build website

on:
  push:
    branches:
      - "main"

jobs:
  build:
    runs-on: ubuntu-latest

    steps:
      - name: checkout
        uses: actions/checkout@v4
      - name: Setup PHP
        uses: shivammathur/setup-php@v2
        with:
          php-version: "7.4"
          extensions: mbstring, intl
          ini-values: post_max_size=256M, max_execution_time=180
      - name: make output dir
        run: |
          mkdir _site
      - name: compile webpage
        run: |
          php book.php > _site/index.html
      - name: copy resources
        run: |
          cp -r css fonts images js bib _site/
      - name: upload artifact
        uses: actions/upload-pages-artifact@v3
        with:
          path: ./_site
          name: github-pages
          retention-days: 1
  deploy:
    needs: build

    # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
    permissions:
      pages: write # to deploy to Pages
      id-token: write # to verify the deployment originates from an appropriate source

    # Deploy to the github-pages environment
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}

    # Specify runner + deployment step
    runs-on: ubuntu-latest
    steps:
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v4