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

Tweaks to bytes, numbers; docs. #1054

Merged
merged 1 commit into from
Nov 29, 2023
Merged

Tweaks to bytes, numbers; docs. #1054

merged 1 commit into from
Nov 29, 2023

Conversation

fare
Copy link
Collaborator

@fare fare commented Nov 26, 2023

No description provided.

Copy link

netlify bot commented Nov 26, 2023

Deploy Preview for elastic-ritchie-8f47f9 ready!

Name Link
🔨 Latest commit cabf856
🔍 Latest deploy log https://app.netlify.com/sites/elastic-ritchie-8f47f9/deploys/656687bbb0fde50008ba6b46
😎 Deploy Preview https://deploy-preview-1054--elastic-ritchie-8f47f9.netlify.app
📱 Preview on mobile
Toggle QR Code...

QR Code

Use your smartphone camera to open QR code link.

To edit notification comments on pull requests, go to your Netlify site configuration.

@vyzo
Copy link
Collaborator

vyzo commented Nov 27, 2023

why is the bootstrap changing here?

@fare
Copy link
Collaborator Author

fare commented Nov 27, 2023

Bootstrap changes are to put fx>=0? and friends in the prelude as you requested.

@vyzo
Copy link
Collaborator

vyzo commented Nov 27, 2023

No need to recompile the bootstrap for this, it is not used in core, no?

Basically if the bootstrap changes I cant cherry pick for 18.1

@fare
Copy link
Collaborator Author

fare commented Nov 27, 2023

No it's not used in core, but it's exported by the prelude. Maybe I don't understand when to bootstrap or not boostrap.

@fare
Copy link
Collaborator Author

fare commented Nov 27, 2023

Reverted the bootstrap changes. PTAL.

Copy link
Collaborator

@chiefnoah chiefnoah left a comment

Choose a reason for hiding this comment

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

LGTM

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.

3 participants