diff options
| author | Gaëtan Gilbert | 2020-02-03 14:49:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-03 14:49:53 +0100 |
| commit | 45f0dc36a749371de35a5d4b998e1305f47e3beb (patch) | |
| tree | ab6351f4918b54529436ab2aa982a0f70209669b /kernel/nativecode.ml | |
| parent | 54f45f5c89f003b4ed2a6e13fdda88d05ee45c83 (diff) | |
| parent | c8ad7e25537d1519646c04b7a35ec53a4c7fae57 (diff) | |
Merge PR #11493: [makefile] Ignore _build_boot directory
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions