Skip to content

Conversation

@strub
Copy link
Member

@strub strub commented Sep 25, 2024

Fix #625

@strub strub added enhancement chore Ungrateful tasks that need done but that nobody wants to do labels Sep 25, 2024
@strub strub requested a review from fdupress September 25, 2024 15:46
@strub strub self-assigned this Sep 25, 2024
@strub strub enabled auto-merge (rebase) September 25, 2024 15:46
@strub strub merged commit a50c7bd into main Sep 25, 2024
@strub strub deleted the fix-625 branch September 25, 2024 15:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

chore Ungrateful tasks that need done but that nobody wants to do enhancement

Projects

None yet

Development

Successfully merging this pull request may close these issues.

The CI should compile with warning-as-errors.

3 participants