Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CI build on branches starting with 'dev**' #931

Merged

Conversation

johnwason
Copy link
Contributor

This PR adds triggers so that branches starting with "dev/" will be built on GitHub actions. This is a convenience when developing on a branch before a pull request is started.

@Levi-Armstrong
Copy link
Contributor

I think we should just remove the branches because this rep only has master.

@johnwason
Copy link
Contributor Author

If you build for all branches a pull request might build twice when you push to a branch that has an open pull request, once for the push and once for the pull request. The solution here is you push to dev/ initially and then to a branch without the prefix for the pull request.

@Levi-Armstrong Levi-Armstrong merged commit 791d4ca into tesseract-robotics:master Sep 4, 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