diff options
| author | Emilio Jesus Gallego Arias | 2018-09-10 10:46:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-20 20:06:36 +0200 |
| commit | 8f23d8d339403006d6464510c7d2cd285cf38b0a (patch) | |
| tree | ababa334c4d40f0386be7ac235eb7b4acae0be6d /Makefile.dune | |
| parent | 4f85e540349004d4f9388a90061fc4a1541d9c40 (diff) | |
[opam] Fix typo in build variable.
Fixes #8431
Diffstat (limited to 'Makefile.dune')
0 files changed, 0 insertions, 0 deletions