Skip to content

Merge branch 'release-v0.7.1' #114

Merge branch 'release-v0.7.1'

Merge branch 'release-v0.7.1' #114

Workflow file for this run

name: MKDocs
on:
push:
branches: [develop]
tags: [v*]
paths:
- .github/workflows/mkdocs.yml
- docs/**
workflow_dispatch:
permissions:
contents: write
jobs:
mkdocs:
name: "Build and Deploy MkDocs to GitHub Pages"
runs-on: ubuntu-latest
steps:
- name: 📥 Checkout repository
uses: actions/checkout@v3
with:
fetch-depth: 0
- name: 🧰 Set up Python
uses: actions/setup-python@v4
with:
python-version: "3.9"
cache: "pip" # caching pip dependencies
- name: 🔨 Install rzk proof assistant
uses: jaxxstorm/[email protected]
with:
repo: rzk-lang/rzk
tag: latest # FIXME: should use the version from the same Git commit
rename-to: rzk
chmod: 0755
- name: 🔨 Install MkDocs Material and mike
run: pip install -r docs/requirements.txt
- name: ⚙️ Configure Git user
run: |
git config --local user.email "github-actions[bot]@users.noreply.github.com"
git config --local user.name "github-actions[bot]"
- name: 🚀 Deploy with mike (${{ github.ref_name }}, latest)
if: ${{ github.ref_name != 'develop' }}
run: |
mike deploy --push --update-aliases --config-file docs/mkdocs.yml ${{ github.ref_name }} latest
- name: 🚀 Deploy with mike (${{ github.ref_name }})
if: ${{ github.ref_name == 'develop' }}
run: |
mike deploy --push --config-file docs/mkdocs.yml ${{ github.ref_name }}