Pin doc deps

2026-08-03 20:14:20 +02:00 · 2026-05-31 20:12:06 -07:00
parent 49780cabbe
commit 6a1d56c425
3 changed files with 507 additions and 1 deletions
@@ -24,7 +24,7 @@ jobs:
      run: |
        sudo apt update
        sudo apt install doxygen
-        pip install mkdocs-material==9.7.0 mkdocstrings==1.0.0 mike==2.1.3 typing_extensions==4.15.0
+        pip install --require-hashes -r support/doc-requirements.txt
        cmake -E make_directory ${{runner.workspace}}/build
        # Workaround https://github.com/actions/checkout/issues/13:
        git config --global user.name "$(git --no-pager log --format=format:'%an' -n 1)"