diff options
| author | Emilio Jesus Gallego Arias | 2019-03-05 13:50:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-05 13:54:35 +0100 |
| commit | c0948de203f6eccb42c47c2e818cf8234f09ec79 (patch) | |
| tree | 20d2e3d7652c2b57816df51effc5057df10b1cca /kernel/nativevalues.ml | |
| parent | b0d35837ff193b66ba37355093b2227f2b1be1ac (diff) | |
[dune] [checker] Don't install internal checker library.
This library is private and shouldn't be exposed to plugins.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions