Make PRs only if a new commit was made. #18

Merged
Philipp merged 2 commits from opt-pr into main 2023-11-21 21:08:25 +01:00
Owner
No description provided.
Philipp added 2 commits 2023-11-21 21:08:01 +01:00
Philipp merged commit 1c9d3972a7 into main 2023-11-21 21:08:25 +01:00
Philipp deleted branch opt-pr 2023-11-21 21:08:26 +01:00
Sign in to join this conversation.
No description provided.