Skip to content

Conversation

henrikjacobsenfys
Copy link
Member

Since the file seems to be unused, we remove it.

@henrikjacobsenfys henrikjacobsenfys added the chore PR label label Jan 20, 2025
@henrikjacobsenfys henrikjacobsenfys merged commit 047e7e0 into develop Jan 20, 2025
34 checks passed
@henrikjacobsenfys henrikjacobsenfys deleted the remove-virtual branch January 20, 2025 13:21
elindgren pushed a commit that referenced this pull request Mar 3, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

chore PR label

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant