Skip to content

cleanup mentioned repos - #85

Merged
pmai merged 1 commit into
masterfrom
84-refresh-mentioned-repos
Nov 13, 2025
Merged

cleanup mentioned repos#85
pmai merged 1 commit into
masterfrom
84-refresh-mentioned-repos

Conversation

@TimmRuppert

@TimmRuppertTimmRuppert commented Nov 11, 2025

Copy link
Copy Markdown
Contributor

Reference to a related issue in the repository

#84

Add a description

  • Removed osi validation
  • Restructured the overview into sections
  • Added osi-cpp and osi-python
  • Added all except the documentation repos to the menu bar dropdown (the thing in the top right)
  • Removed old comments

Check the checklist

  • I have performed a self-review of my own code/documentation.
  • My documentation changes are related to another repository in the organization. Here is the link to the issue/repo.
  • My changes generate no new warnings during the documentation generation.
  • The Antora pipeline which pushes the documentation to gh-pages on the downstream repository passes with my changes.

Signed-off-by: Timm Ruppert <timm.ruppert@persival.de>
@pmai

pmai commented Nov 13, 2025

Copy link
Copy Markdown
Contributor

CCB 2025-11-13: Merge as-is.

@asadekasamasadekasam added the ReadyToMerge This PR has been approved to merge and will be merged by a member of the CCB. label Nov 13, 2025
@pmai
pmai merged commit dbdca16 into masterNov 13, 2025
1 check passed
@pmai
pmai deleted the 84-refresh-mentioned-repos branch November 13, 2025 11:51
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ReadyToMergeThis PR has been approved to merge and will be merged by a member of the CCB.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants

@TimmRuppert@pmai@jdsika@thomassedlmayer@asadekasam