Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Oct 25, 2024

Similarly to #1575 because intDomain.ml is the largest file we have.

They are moved to a new int subdirectory. There's also a IntDomain0 with all the various interfaces and their adapters.
The splitting is done such that git blame history is preserved for default git settings. Thus the git graph is a bit of a braid.

@sim642 sim642 added the cleanup Refactoring, clean-up label Oct 25, 2024
@sim642 sim642 added this to the v2.5.0 milestone Oct 25, 2024
@sim642 sim642 removed this from the v2.5.0 milestone Nov 26, 2024
@sim642 sim642 added this to the v2.6.0 milestone Nov 26, 2024
@michael-schwarz michael-schwarz self-requested a review December 15, 2024 15:35
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

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

Do we need to wait on anything here, or should we just go ahead and merge before it gets stale?

Adapting other PRs to this is probably easier than recreating this with all the history preservation things.

@sim642 sim642 merged commit d2f6584 into master Dec 16, 2024
20 checks passed
@sim642 sim642 deleted the intdomain-split branch December 16, 2024 09:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants