Closed gridbugs closed 2 days ago
We should copy this file into this repo in case its location on dune.build's server changes, but I'm not sure where to put it.
I have incorporated your change in #61 in this commit (added you as co-author). Consequently, closing this PR.
We should copy this file into this repo in case its location on dune.build's server changes, but I'm not sure where to put it.