Skip to content

Conversation

@mgajda
Copy link

@mgajda mgajda commented Feb 26, 2023

Since #1551 has took some time, there was duplicate instance.

This PR just removes the duplicate.

@mgajda
Copy link
Author

mgajda commented Feb 26, 2023

@tchoutri @hasufell Fixed the branch.

@tchoutri
Copy link
Contributor

Hey, this is actually a duplicate of #1652 but since it's pressing I'll merge my own PR :)

@tchoutri
Copy link
Contributor

The PR is merged, you can use HEAD now :)

@tchoutri tchoutri closed this Feb 26, 2023
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.

2 participants