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.

Sign up for GitHub

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

Jump to bottom

main: port from dev #4481

Merged
merged 1 commit into from
Mar 22, 2025
Merged

main: port from dev #4481

merged 1 commit into from
Mar 22, 2025
+83 −82

Conversation

ralfhandl
Copy link
Contributor

@ralfhandl ralfhandl commented Mar 20, 2025 •
edited
Loading

Port workflows and scripts from dev to avoid:

  • breaking scripts on dev when changing something on `main,
  • possible problems with merging release branches.

The four changed files contain the contents from dev, the deleted file was already deleted on dev.

Tick one of the following options:

  • schema changes are included in this pull request
  • schema changes are needed for this pull request but not done yet
  • no schema changes are needed for this pull request

@ralfhandl ralfhandl requested review from a team as code owners March 20, 2025 18:36
@ralfhandl ralfhandl added script Pull requests that update Bash or JavaScript code approved pr port PRs that just port an approved PR to another version Housekeeping labels Mar 20, 2025
@miqui miqui merged commit e09c356 into OAI:main Mar 22, 2025
2 checks passed
@ralfhandl ralfhandl deleted the main-sync-scripts-from-dev branch March 24, 2025 08:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@miqui miqui

Assignees
No one assigned
Labels
approved pr port PRs that just port an approved PR to another version Housekeeping script Pull requests that update Bash or JavaScript code
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@ralfhandl @miqui