docs-dev.yml

name: Publish Dev Docs

on:
  push:
    branches:
      - main

jobs:
  publish:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository
        uses: actions/checkout@v5
        with:
          fetch-depth: 0

      - name: Setup packages
        uses: ./.github/actions/setup

      - name: Get variables
        run: |
          python -c 'import pathpyG; print(f"package_version={pathpyG.__version__}")' >> "$GITHUB_ENV"
          echo "sha_short=$(git rev-parse --short "$GITHUB_SHA")" >> "$GITHUB_ENV"

      - name: Publish docs
        # First configure git correctly
        # Then use the alias of the current dev version to delete it based on its identifier
        # Then deploy the new version so that there is only one dev version at a time
        run: |
          git config user.name github-actions
          git config user.email github-actions@github.com
          git fetch origin gh-pages --depth=1
          mike delete --push $(mike list | grep dev | awk '{print $1}' | tr -d '()')
          mike deploy --push --update-aliases "${{ env.package_version }}-dev" dev
          mike set-default --push --allow-empty dev