diff options
| author | Emilio Jesus Gallego Arias | 2018-10-01 04:44:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-01 04:44:27 +0200 |
| commit | 2b2b10cd5bf017d9b69076ea98e4a1cb77fdbc00 (patch) | |
| tree | 5b9900d901959f65dcaf09df04e8448caca3f4a0 /kernel/nativelambda.ml | |
| parent | c155259dee7e4b2bfafe42375b45f2f4d6c6cfbd (diff) | |
[dune] [configure] Fix typo in default prefix setting.
Fix silly typo that created havoc in developer out-of-the-box setups.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions