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

[Merged by Bors] - feat: more consistent use of ext, and updating porting notes. #5242

Closed
wants to merge 9 commits into from

Conversation

semorrison
Copy link
Contributor


Open in Gitpod

@semorrison semorrison added awaiting-review The author would like community review of the PR awaiting-CI labels Jun 19, 2023
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@semorrison semorrison added ready-to-merge This PR has been sent to bors. merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed awaiting-review The author would like community review of the PR labels Jun 19, 2023
@bors
Copy link

bors bot commented Jun 19, 2023

Merge conflict.

@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jun 19, 2023
Scott Morrison added 2 commits June 20, 2023 11:44
@semorrison
Copy link
Contributor Author

bors merge

bors bot pushed a commit that referenced this pull request Jun 20, 2023
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
@bors
Copy link

bors bot commented Jun 20, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: more consistent use of ext, and updating porting notes. [Merged by Bors] - feat: more consistent use of ext, and updating porting notes. Jun 20, 2023
@bors bors bot closed this Jun 20, 2023
@bors bors bot deleted the hom_ext branch June 20, 2023 05:36
semorrison added a commit that referenced this pull request Jun 20, 2023
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
alexkeizer pushed a commit that referenced this pull request Jun 22, 2023
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
semorrison added a commit that referenced this pull request Jun 23, 2023
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
semorrison added a commit that referenced this pull request Jun 25, 2023
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
semorrison added a commit that referenced this pull request Jun 28, 2023
feat: more consistent use of `ext`, and updating porting notes. (#5242)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

feat: port Probability.Martingale.Upcrossing (#5281)

feat: port Probability.Martingale.BorelCantelli (#5285)

blegh

merge from hack branch

rebase is crap

not there yet

chore: better TypeMax instances for limits in Type

last changes from _hack branch

long line
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants