Skip to content

Merge compatible into develop #17541

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

Open
wants to merge 450 commits into
base: develop
Choose a base branch
from

Conversation

Geometer1729
Copy link
Member

Merges latest compatible into develop (automatic merge, no conflicts)

dannywillems and others added 30 commits July 1, 2025 21:54
Co-authored-by: Danny Willems <be.danny.willems@gmail.com>
More informative snark pool verification errors
…register

Exit_handlers: remove unused method
This should be inoffensive. This is mostly to get the latest features of OPAM,
in case we need it.
…n_folder

[Clean up] remove unused automation folder with obsoleted tools
…m_legacy_builds

generate legacy packages for bookworm
Dockerfiles/scripts: adding jammy toolchain
@Geometer1729
Copy link
Member Author

!ci-build-me

@Geometer1729 Geometer1729 marked this pull request as ready for review July 15, 2025 17:16
@dkijania
Copy link
Member

Looks good. Can you run nightly to double check everything is in order?

@Geometer1729
Copy link
Member Author

!ci-nightly-me

@dannywillems
Copy link
Member

!ci-bypass-changelog

@Geometer1729
Copy link
Member Author

Geometer1729 commented Jul 16, 2025

!ci-build-me
!ci-nightly-me
Edit:(this doesn't work ☹️ )

@Geometer1729
Copy link
Member Author

!ci-build-me

@Geometer1729
Copy link
Member Author

!ci-nightly-me

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.

6 participants