Skip to content

Fix build #317

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 4 commits into from
Mar 17, 2025
Merged

Fix build #317

merged 4 commits into from
Mar 17, 2025

Conversation

MattiSG
Copy link
Member

@MattiSG MattiSG commented Mar 17, 2025 •
edited by bonjourmauko
Loading

@MattiSG MattiSG requested a review from verbman March 17, 2025 06:52
verbman and others added 2 commits March 17, 2025 14:53
@MattiSG
Copy link
Member Author

MattiSG commented Mar 17, 2025

I use admin privileges to bypass review in order to enable deployment of #316 and fix deployment that fails since #315. This is done at the cost of less documentation being automatically generated, but right now the documentation is anyway obsolete.

@MattiSG MattiSG merged commit a6e8c5d into main Mar 17, 2025
3 checks passed
@MattiSG MattiSG deleted the fix-build branch March 17, 2025 15:02
bonjourmauko added a commit that referenced this pull request Mar 17, 2025
@bonjourmauko
revert: changes from #317
ff0b7c2
@bonjourmauko bonjourmauko mentioned this pull request Mar 17, 2025
Merged
@MattiSG MattiSG mentioned this pull request Apr 18, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@verbman verbman Awaiting requested review from verbman

Assignees

@verbman verbman

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@MattiSG @verbman