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.

Sign up for GitHub

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

Jump to bottom

update for jsoo#883 #40

Merged
merged 2 commits into from
Dec 22, 2019
Merged

update for jsoo#883 #40

merged 2 commits into from
Dec 22, 2019

Conversation

hhugo
Copy link
Contributor

@hhugo hhugo commented Oct 11, 2019 •
edited
Loading

@hhugo hhugo changed the title update for jsoo#883 (WIP) update for jsoo#883 Nov 11, 2019
@hhugo
Copy link
Contributor Author

hhugo commented Nov 11, 2019

Jsoo has been released. Release/Review this whenever you have time.

@hhugo
Copy link
Contributor Author

hhugo commented Dec 21, 2019

Gentle ping

@rgrinberg
Copy link
Collaborator

Thanks Hugo. The PR looks good.

@rgrinberg rgrinberg merged commit 9949c47 into inhabitedtype:master Dec 22, 2019
@seliopou
Copy link
Member

I'm not quite sure the right way to constraint the JSOO version in the OPAM file. Any guidance on that @hhugo? Use conflicts?

@hhugo
Copy link
Contributor Author

hhugo commented Jan 30, 2020

conflicts looks appropriate

@hhugo hhugo deleted the jsoo-883 branch January 30, 2020 16:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@hhugo @rgrinberg @seliopou