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

fix(engine) Fix naming bundle regression #1286

Merged
merged 6 commits into from
Feb 5, 2025

Conversation

maximebuyse
Copy link
Contributor

Fixes #1283 and more small regressions from #1199.

One of the fixes should be temporary, I opened #1285 to track this.

@maximebuyse maximebuyse requested a review from W95Psp February 3, 2025 16:24
@maximebuyse maximebuyse self-assigned this Feb 3, 2025
@maximebuyse maximebuyse requested a review from a team as a code owner February 3, 2025 16:24
engine/lib/dependencies.ml Outdated Show resolved Hide resolved
Copy link
Collaborator

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

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

Looks good, I have one nit.
Also, are the changes to proof-libs related to the changes of dependencies from this PR?

@maximebuyse
Copy link
Contributor Author

Looks good, I have one nit. Also, are the changes to proof-libs related to the changes of dependencies from this PR?

Thanks for the suggestion, it looks better. The proof-libs changes are not really related to the other changes but they also fix a naming regression.

Copy link
Collaborator

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

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

Ok, no problem, the lib changes are fairly small, let's merge! :)

@maximebuyse maximebuyse enabled auto-merge February 5, 2025 09:48
@maximebuyse maximebuyse added this pull request to the merge queue Feb 5, 2025
Merged via the queue into main with commit 321a613 Feb 5, 2025
15 checks passed
@maximebuyse maximebuyse deleted the fix-naming-bundle-regression branch February 5, 2025 10:40
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.

Import of name from bundle that doesn't exist
2 participants