Skip to content

Remove obsolete/unmaintained ports - #8788

Merged
asfernandes merged 1 commit into
masterfrom
work/ports-cleanup
Oct 26, 2025
Merged

Remove obsolete/unmaintained ports#8788
asfernandes merged 1 commit into
masterfrom
work/ports-cleanup

Conversation

@asfernandes

Copy link
Copy Markdown
Member

No description provided.

@asfernandes asfernandes self-assigned this Oct 23, 2025
@asfernandes
asfernandes merged commit 5c57dcd into master Oct 26, 2025
46 checks passed
@asfernandes
asfernandes deleted the work/ports-cleanup branch October 26, 2025 17:45
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