Skip to content

Conversation

@jrochel
Copy link

@jrochel jrochel commented Jul 26, 2021

No description provided.

@jrochel jrochel requested a review from Zzull July 26, 2021 13:16
@Zzull Zzull merged commit c797386 into master Jul 26, 2021
@Zzull Zzull deleted the opam branch July 26, 2021 16:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants