diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-05-05 14:05:12 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-05-05 14:05:12 -0400 |
| commit | a2a249211c2ac1e18eff0d4f28e5afc98c137f97 (patch) | |
| tree | f426e3d9befe93ebfc24d00a37c11d6953068099 /library/global.ml | |
| parent | 1432318faa4cb6a50eca2c7a371b43b3b9969666 (diff) | |
Fix install target in Makefile after 6acf543800fe176ca7d47ef7165ebc14588efb6f.
Should decrease the noise level in the bench.
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions