Skip to content

Modernize stdlib #1764

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

Merged
merged 3 commits into from
Dec 30, 2024
Merged

Modernize stdlib #1764

merged 3 commits into from
Dec 30, 2024

Conversation

hhugo
Copy link
Member

@hhugo hhugo commented Dec 10, 2024

and remove modern_stdlib.js

@hhugo hhugo requested a review from TyOverby December 10, 2024 09:41
@hhugo hhugo assigned hhugo and TyOverby and unassigned hhugo Dec 11, 2024
@hhugo
Copy link
Member Author

hhugo commented Dec 12, 2024

@TyOverby, any opinion ?

@hhugo hhugo added this to the 6.0 milestone Dec 13, 2024
@TyOverby
Copy link
Collaborator

I think we may have moved away from stdlib_modern for performance reasons; I can check when I get back to work in January

@hhugo hhugo added the blocked label Dec 17, 2024
@smorimoto smorimoto requested a review from Copilot December 28, 2024 17:36
Copy link

@Copilot Copilot AI left a comment

Choose a reason for hiding this comment

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

Copilot reviewed 3 out of 7 changed files in this pull request and generated 1 comment.

Files not reviewed (4)
  • compiler/lib-runtime-files/tests/all.ml: Language not supported
  • compiler/tests-compiler/gh1051.ml: Language not supported
  • compiler/tests-compiler/util/util.ml: Language not supported
  • compiler/tests-compiler/util/util.mli: Language not supported

@ocsigen ocsigen deleted a comment from Copilot AI Dec 30, 2024
@TyOverby
Copy link
Collaborator

Looks like we're using modern anyway

@smorimoto smorimoto removed the blocked label Dec 30, 2024
@hhugo hhugo merged commit e734c24 into master Dec 30, 2024
28 checks passed
@hhugo hhugo deleted the modern-stdlib branch December 30, 2024 20:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants