Skip to content

Comment out public/docs directory creation - #472

Merged
joergwa merged 1 commit into
mainfrom
joergwa-patch-2
Jul 30, 2026
Merged

Comment out public/docs directory creation#472
joergwa merged 1 commit into
mainfrom
joergwa-patch-2

Conversation

@joergwa

@joergwa joergwa commented Jul 30, 2026

Copy link
Copy Markdown
Collaborator

Comment out the creation of public/docs directory and the copy command for HTML docs.

Comment out the creation of public/docs directory and the copy command for HTML docs.
@joergwa
joergwa merged commit b4ce63e into main Jul 30, 2026
1 of 2 checks passed
@github-actions

Copy link
Copy Markdown
Contributor

PMDco Quality Check

Auto-added annotations

No annotations were auto-added.

Hygiene issues

No issues found — all terms conform.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant