diff options
| author | Hugo Herbelin | 2016-10-11 22:40:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-17 20:14:13 +0200 |
| commit | 12f9dbf211b7ee27aecda09cf4209084ccaae5a6 (patch) | |
| tree | 1903c35e22b43bd6634367a34ac38fac8c306fac /kernel/nativecode.ml | |
| parent | 9603b9996c717b52e95626ea69fe9b05a89f4738 (diff) | |
Grouping checks about commands together.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions