Skip to content

feat(IdS): add JML basics #401

feat(IdS): add JML basics

feat(IdS): add JML basics #401

Workflow file for this run

name: Deploy site to GitHub Pages
on:
push:
branches: ["main"]
paths:
- "*/*.md"
- "*/*.jpg"
- "*/*.jpeg"
- "*/*.webp"
- "*/*.png"
- "*/*.gif"
- "*/*.html"
- "index.html"
- "template.html"
- ".github/workflows/gh-pages.yml"
workflow_dispatch:
permissions:
contents: read
pages: write
id-token: write
concurrency:
group: "pages"
cancel-in-progress: true
jobs:
# TODO: fix permissions so we don't need to do everything as root
build:
runs-on: ubuntu-latest
container:
image: ghcr.io/${{ github.repository }}-build-tools:latest
options: --user root
env:
LC_ALL: it_IT.utf8
LANG: it_IT.utf8
volumes:
- ${{ github.workspace }}:/workspace
environment: github-pages
steps:
- name: Checkout
uses: actions/checkout@v3
with:
fetch-depth: 0
- name: Add safe directory
run: |
git config --global --add safe.directory /workspace
- uses: chetan/git-restore-mtime-action@v2
with:
working-directory: '/workspace'
- name: Build docs & create index.html
shell: bash
working-directory: /workspace
run: |
sudo /root/build_docs_v2.py
- name: Delete symlinks if any # I don't remember why I added this 17 months ago
run: |
find . -type l -delete
- name: Upload artifact
uses: actions/upload-pages-artifact@v3
with:
name: github-pages-${{ github.sha }}
path: ./
deploy:
needs: build
permissions:
pages: write
id-token: write
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
runs-on: ubuntu-latest
steps:
- name: Setup Pages
uses: actions/configure-pages@v5
- name: List artifacts
id: list
uses: yakubique/list-artifacts@v1
with:
name: test-*
- name: Download artifact
uses: actions/download-artifact@v4
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v4
with:
artifact_name: github-pages-${{ github.sha }}