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

warning 58 #3

Open
wants to merge 13 commits into
base: master
Choose a base branch
from
Open

warning 58 #3

wants to merge 13 commits into from

Conversation

Sylvain78
Copy link

It removes the warning 58 when compiling with dune

@phated
Copy link
Member

phated commented Dec 12, 2020

I just realized I wasn't watching this repo. Sorry about that! I'll get this merged and released this weekend!

@phated phated self-assigned this Dec 12, 2020
@phated
Copy link
Member

phated commented Jan 14, 2021

@Sylvain78 Just wanted to check on the status of this. I noticed you pushed some commits recently.

I've been focused on getting our CI setup working so we don't linger on things like this in the future and it is looking pretty good, so I'll be able to pull this in very soon (and get it published on opam).

@Sylvain78
Copy link
Author

@phated Could you advance on your CI setup, in order to merge my pull request ?

@ospencer
Copy link
Member

@Sylvain78 Could you remove the additional commits that you added?

@Sylvain78
Copy link
Author

@Sylvain78 Could you remove the additional commits that you added?

I don't know how to remove commits. But as the only concerned commit for the warning 58 is a one liner, maybe you could apply it yourself, and close my pull request ?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@phated phated

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Sylvain78 @phated @ospencer