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

Include random.gd before coll.gi #2205

Merged
merged 1 commit into from
Feb 23, 2018

Conversation

fingolfin
Copy link
Member

This way, we can move the definition of GlobalMersenneTwister from
coll.gi to random.gd, and will be able to use InstallMethodWithRandomSource
inside of coll.gi

This implements a change I suggested on #2204 -- if @ChrisJefferson likes it, also feel free to cherry-pick this into your PR, and then we just test and merge your PR and we close this. Or we merge this first. Or we discard this PR if people hate it, and do something completely different ;-).

This way, we can move the definition of GlobalMersenneTwister from
coll.gi to random.gd, and will be able to use InstallMethodWithRandomSource
inside of coll.gi
@fingolfin fingolfin added topic: library release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes labels Feb 23, 2018
@ChrisJefferson
Copy link
Contributor

ChrisJefferson commented Feb 23, 2018

This seems like a reasonable change, but it desn't merge well with my PR, so we should merge this, then I throw my PR away and start again.

@fingolfin
Copy link
Member Author

If you are willing to do that: fine by me, thanks, and sorry for the extra work

@fingolfin
Copy link
Member Author

BTW, I don't think it is that incompatible: the first commit of your PR should not conflict at all, and the second just needs the "a (finite) collection" method installation moved back to coll.gi, no?

I could also do that, and add your commits to this PR, then you have no further work. Just let me know what you prefer (i.e. either merge this PR then rebase yours, or tell me to merge your work into this PR).

@ChrisJefferson
Copy link
Contributor

I'll merge this and fix, my PR has other problems (some infinite loop is happening)

@ChrisJefferson ChrisJefferson merged commit 880bf19 into gap-system:master Feb 23, 2018
@fingolfin fingolfin deleted the mh/reorder-random branch February 23, 2018 21:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes topic: library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants