Fix 'make install' (#839)
Signed-off-by: Jeremie Dimino <jdimino@janestreet.com>
This commit is contained in:
parent
e45e431588
commit
f70b137640
Loading…
Reference in New Issue