Skip to content

Conversation

rgrinberg
Copy link
Member

This makes it easier to maintain external patches

cc @awilliambauer

Signed-off-by: Rudi Grinberg me@rgrinberg.com

This makes it easier to maintain external patches

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

<!-- ps-id: 3e5a71be-66d3-4edc-a645-fed7dd054064 -->
@rgrinberg rgrinberg merged commit 03bbe54 into master Jul 9, 2024
@rgrinberg rgrinberg deleted the ps/rr/chore__switch_to_janestreet_style branch July 9, 2024 20:44
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.

1 participant