Update docs (mostly), fixes, etc
Some checks failed
Update docs / build_docs (push) Has been cancelled
Update helpers / build_helpers (push) Successful in 25s

This commit is contained in:
2026-02-21 16:24:21 +01:00
parent 2a592753bf
commit baebaa99d0
45 changed files with 1038 additions and 691 deletions

View File

@@ -0,0 +1,35 @@
name: Update helpers
on:
push:
paths:
- 'src/**'
jobs:
build_helpers:
runs-on: ubuntu-latest
steps:
- name: Set up Git repository
uses: actions/checkout@v6
- name: Sign into gitea registry
uses: https://github.com/docker/login-action@v3
with:
username: ${{ vars.REGISTRY_USER_USERNAME }}
password: ${{ secrets.REGISTRY_USER_PASSWORD }}
registry: ${{ vars.REGISTRY_BASE_URL }}
- name: Run format of main
uses: actions/latex-format@main
with:
workdir: main
- name: Run format of extra
uses: actions/latex-format@main
with:
workdir: extra
- name: Run build
run: ./build.sh
- name: Upload compiled helpers
uses: actions/git-auto-commit-action@v7
with:
commit_message: "[skip ci] Build helpers on push"
commit_user_name: Helpers compiler [bot]
commit_user_email: actions@janishutz.com
commit_author: Helpers compiler [bot] <actions@janishutz.com>
push_options: "--force"