Skip to content

Conversation

fiseni
Copy link
Collaborator

@fiseni fiseni commented Jul 24, 2023

No description provided.

@fiseni
Copy link
Collaborator Author

fiseni commented Jul 24, 2023

@ardalis The PR triggered the correct workflow.

On merge, this will run again. If you protect the main branch, so we're sure nobody can push directly to the main, then perhaps we don't need the push trigger. It doesn't hurt, but it's just wasting resources.

@fiseni
Copy link
Collaborator Author

fiseni commented Jul 24, 2023

Actually, we should leave it as it is. We should run it on merge too, so the builds are visible on the commit history. That affects the badges I assume, so better to have it.

@ardalis ardalis merged commit 6405783 into main Jul 24, 2023
@fiseni fiseni deleted the fiseni/dummy branch July 24, 2023 16:23
This was referenced Jul 31, 2025
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