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

[AUTO-MERGE] Merge main into develop via merge-main-to-develop #3271

Closed
wants to merge 0 commits into from

Conversation

idanov
Copy link
Member

@idanov idanov commented Nov 4, 2023

A new change in main cannot be merged into develop as part of the regular sync job, hence this PR. Please resolve the conflicts manually, and make sure to obtain 2 approvals once the builds pass.

IMPORTANT NOTICE

Please let CircleCI merge this PR automatically, with merge commit enabled.

@noklam
Copy link
Contributor

noklam commented Nov 7, 2023

There are many changes to dataset which shouldn't exist anymore.

@noklam noklam closed this Nov 7, 2023
@noklam noklam force-pushed the merge-main-to-develop branch from ab4bc50 to 1fb906c Compare November 7, 2023 05:32
@noklam noklam deleted the merge-main-to-develop branch November 7, 2023 05:33
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