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

Remove fold on ephemerons #12

Merged
merged 4 commits into from
Sep 25, 2023
Merged

Conversation

nberth
Copy link
Collaborator

@nberth nberth commented Sep 15, 2023

Before this change we had a warning about a function not being available in OCaml 5.

@nberth nberth added the invalid This doesn't seem right label Sep 15, 2023
@nberth nberth force-pushed the remove-weak-fold branch 2 times, most recently from e532a7a to 0c95ca5 Compare September 19, 2023 07:46
@nberth nberth marked this pull request as ready for review September 19, 2023 07:46
@nberth nberth added ok to review As its name says and removed invalid This doesn't seem right labels Sep 19, 2023
@nberth nberth changed the title Remove weak fold Remove fold on ephemerons Sep 19, 2023
@nberth nberth marked this pull request as draft September 21, 2023 14:13
@nberth nberth marked this pull request as ready for review September 21, 2023 14:14
@lefessan
Copy link
Member

There are too many unrelated commits in this PR. If you want a review, I think it needs to be splitted in multiple simpler PRs. Typically, changes to drom files that modify many generated files should be done in a specific PR, with a single commit containing all the changes to generated files.

@nberth nberth force-pushed the remove-weak-fold branch 2 times, most recently from d2aefa1 to 2f1306f Compare September 22, 2023 08:29
@nberth nberth mentioned this pull request Sep 22, 2023
@CLAassistant
Copy link

CLAassistant commented Sep 22, 2023

CLA assistant check
All committers have signed the CLA.

@nberth nberth merged commit f4d5b99 into OCamlPro:master Sep 25, 2023
3 checks passed
@nberth nberth deleted the remove-weak-fold branch September 25, 2023 14:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ok to review As its name says
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants