Skip to content

Merge branch 'main' into peterhher/add-star-page #468

Merge branch 'main' into peterhher/add-star-page

Merge branch 'main' into peterhher/add-star-page #468

Workflow file for this run

name: CI-CD
# run on any push to any directory and a pull to main or development
on:
push:
pull_request:
branches:
- main
- development
jobs:
################################################################################################
# Docs: Build and deploy mkdocs documentation
################################################################################################
Docs:
runs-on: ubuntu-latest
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
permissions:
# Need to give the action permission to write to the repository to deploy the docs
contents: write
strategy:
matrix:
os: [ubuntu-latest]
steps:
- name: Check-out repository
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: Configure Git Credentials
run: |
git config user.name github-actions[bot]
git config user.email github-actions[bot]@users.noreply.github.com
- name: Install Pixi
uses: prefix-dev/[email protected]
with:
pixi-version: v0.34.0
cache: true
locked: false
- name: Build documentation
run: pixi run build
- name: Build and deploy documentation (only on push to main)
if: github.ref == 'refs/heads/main' && github.event_name == 'push'
run: pixi run mike deploy --push dev devel