diff options
| author | Théo Zimmermann | 2020-02-14 17:12:47 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-14 17:12:47 +0100 |
| commit | df94f1a5430dde7cee6ccb1c16854bcbc94575c8 (patch) | |
| tree | 53de58ca4f8a7281eecd41ee476843e3d6e59d19 /Makefile.dev | |
| parent | 90ccf8e413aea57ec670ea26174d3deffb4036aa (diff) | |
| parent | 8d03696658e409df1349585d59dabe13dbf52ed2 (diff) | |
Merge PR #11468: [doc] fix typo & update release-process.md for opam/docker packaging
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions