0.12.0-17 docs

2026-03-30 19:24:50 +00:00
parent 6b1532d8ad
commit 7d5422b9f7
90 changed files with 19 additions and 8532 deletions
@@ -89,15 +89,29 @@ jobs:
          mkdir -p .worktrees
          git worktree add --detach .worktrees/main "${MAIN_REF}"

-          mkdocs build --strict --verbose \
+          if ! mkdocs build --strict --verbose \
            --config-file .worktrees/main/mkdocs.yml \
-            --site-dir site
+            --site-dir site; then
+            echo "::error::Main-Dokumentation konnte nicht gebaut werden."
+            exit 1
+          fi

          if [ -n "${DEV_REF}" ]; then
            git worktree add --detach .worktrees/dev "${DEV_REF}"
-            mkdocs build --strict --verbose \
+            if ! mkdocs build --strict --verbose \
              --config-file .worktrees/dev/mkdocs.yml \
-              --site-dir site/dev
+              --site-dir site/dev; then
+              echo "::warning::Dev-Dokumentation konnte nicht gebaut werden. Es wird ein Platzhalter unter /dev erzeugt."
+              rm -rf site/dev
+              mkdir -p site/dev
+              cat > site/dev/index.html <<'EOF'
+          <!doctype html>
+          <html lang="de">
+          <head><meta charset="utf-8"><title>Dev Doku</title></head>
+          <body><p>Dev-Dokumentation ist aktuell auf GitHub noch nicht verfügbar.</p></body>
+          </html>
+          EOF
+            fi
          else
            mkdir -p site/dev
            cat > site/dev/index.html <<'EOF'