Skip to content

Conversation

RobPasMue
Copy link
Member

As title says. This needs to be merged independently to prevent other PRs from failing right away.

@RobPasMue
Copy link
Member Author

Extracted from #144

@github-actions github-actions bot added the bug Defects or glitches reported by users or developers label Apr 17, 2023
Copy link
Member

@jorgepiloto jorgepiloto left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for adding this, @RobPasMue. Approving and merging 🚀

@jorgepiloto
Copy link
Member

Documentations failures are due to an internal issue in the GitHub CI/CD runners. Merging this.

@jorgepiloto jorgepiloto enabled auto-merge (squash) April 17, 2023 12:04
@jorgepiloto jorgepiloto disabled auto-merge April 17, 2023 12:05
@RobPasMue RobPasMue merged commit f080d11 into main Apr 17, 2023
@RobPasMue RobPasMue deleted the fix/remove-codecov branch April 17, 2023 12:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Defects or glitches reported by users or developers
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants