diff options
| author | Gaëtan Gilbert | 2018-08-28 13:03:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-08-28 13:03:43 +0200 |
| commit | 35c28d8c506e1bb4d9b2f2afa6f2702aa359dc13 (patch) | |
| tree | 204a2458b21dca908a34e625c6cefa711c053703 /kernel/nativevalues.ml | |
| parent | f885e8a88620351d9dc4b0969f520d13197f2184 (diff) | |
Put camldevfiles targets in Makefile
There's no need to build dependencies for it.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions