Skip to content

feat(IdS): multithreading: wait/notify #344

feat(IdS): multithreading: wait/notify

feat(IdS): multithreading: wait/notify #344

Workflow file for this run

name: Deploy site to GitHub Pages
on:
# Runs on pushes targeting the default branch
push:
branches: ["main"]
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
contents: read
pages: write
id-token: write
# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued.
# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete.
concurrency:
group: "pages"
cancel-in-progress: true
jobs:
# Build job
build:
if: '!contains(github.event.head_commit.message, ''skip ci'')'
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
shell: bash
run: |
export HOME=/root
cd /workspace
export PWD=/workspace
git config --global --add safe.directory /workspace # we need to do this again because new login home who dis
echo ----------------------------------
echo User: `whoami`
echo UID: `id -u`
echo GID: `id -g`
echo HOME: $HOME
echo CWD: `pwd`
echo "ENV:"
env
echo ----------------------------------
find . -type f -name "*.md" -mindepth 2 -print0 | while read -d $'\0' doc
do
echo "Processing ${doc}..."
output_dir=$(dirname "${doc}")
output_dir_name=$(basename "${output_dir}")
output_html="${output_dir}/"
output_html+=$(basename "${doc}" .md)
output_html+=".html"
lm_date=$(LC_ALL=it_IT.utf8 git log -1 --format=%ad --date=format:'%d %B %Y' -- "${doc}")
pandoc --template "template.html" -F mermaid-filter --toc --katex="https://cdn.jsdelivr.net/npm/[email protected]/dist/" --metadata "toc-title=Indice" --metadata "lang=it" --metadata "date=${lm_date}" --verbose -o "${output_html}" "${doc}"
done
- name: Create index.html
run: |
find . -type d -mindepth 1 -maxdepth 1 -print0 | sort -z | while read -d $'\0' dir
do
if [[ -f "${dir}/index.html" ]]; then
sed -i "s@{{{PLACEHOLDER}}}@<li><a href=\"${dir}/index.html\">$(basename "${dir}")</a></li>{{{PLACEHOLDER}}}@" index.html
fi
done
sed -i "s@{{{PLACEHOLDER}}}@@g" index.html
- name: Delete symlinks if any
run: |
find . -type l -delete
- name: Upload artifact
uses: actions/upload-pages-artifact@v3
with:
name: github-pages-${{ github.sha }}
path: ./
# Deploy job
deploy:
if: '!contains(github.event.head_commit.message, ''skip ci'')'
# Add a dependency to the build job
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
#actions: write # to download the artifact
# 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: 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 }}