diff options
| author | Maxime Dénès | 2019-04-04 13:22:52 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-04 13:23:55 +0200 |
| commit | 8e4004013182df73f0a0e8521583cd4f79a3ca66 (patch) | |
| tree | aeaead4a8729a46efcde0334b1a79a6422e760ad /kernel/nativecode.mli | |
| parent | 32080d6fe63f2af723decd618bdb8867703e084a (diff) | |
[CI] Fix build of math-comp dependencies
We were incorrectly calling the global `install` target even when
building only subcomponents of the library.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions