Open
Description
For some reason janestreet/bin_prot#29 was not merged with d87bb8f.
I'm not familiar with opam, this may have been done with purpose. In case this was just an oversight, commit 5c8da83 is probably obsolete as well.
Metadata
Metadata
Assignees
Labels
No labels