diff options
| author | Alasdair Armstrong | 2019-05-22 16:19:37 +0100 |
|---|---|---|
| committer | GitHub | 2019-05-22 16:19:37 +0100 |
| commit | 925d976d0a62f61cdc041233af81e20bb56deb00 (patch) | |
| tree | 75059efe1885d0111235ce6b134ca86d7f412776 /src | |
| parent | 0dd3583a0720beeae35432e908ea0c9899d300d7 (diff) | |
Use opam instructions in INSTALL.md
Move the instructions to build everything from source to the wiki
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions