Skip to content

[GH] Use pull_request default events#11

Merged
jplehr merged 1 commit intotudasc:develfrom
jplehr:feat/ghci-use-default-pr-events
Apr 3, 2025
Merged

[GH] Use pull_request default events#11
jplehr merged 1 commit intotudasc:develfrom
jplehr:feat/ghci-use-default-pr-events

Conversation

@jplehr
Copy link
Member

@jplehr jplehr commented Apr 2, 2025

No description provided.

@jplehr jplehr requested a review from pearzt April 2, 2025 21:55
@jplehr jplehr force-pushed the feat/ghci-use-default-pr-events branch from c71cbe8 to 6590680 Compare April 2, 2025 22:06
@jplehr
Copy link
Member Author

jplehr commented Apr 2, 2025

I think we want to have the default behavior (from docs):

For example, if no activity types are specified, the workflow runs when a pull request is opened or reopened or when the head branch of the pull request is updated.

Previously it would not trigger on all events that we care about.

Copy link
Member

@sebastiankreutzer sebastiankreutzer left a comment

Choose a reason for hiding this comment

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

LGTM

@jplehr jplehr merged commit a8d6b5b into tudasc:devel Apr 3, 2025
2 checks passed
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