diff options
| author | Guillaume Melquiond | 2016-01-06 14:49:31 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-01-06 14:49:31 +0100 |
| commit | d0d46d9c5a93de25ecf0202a0ab3dbd83f1ed693 (patch) | |
| tree | 56e40e794519da0ad1d8d377907a9b39a9d2de2c /kernel/nativecode.ml | |
| parent | 1afa595012bbaf5fb89398b355f16159e1af399b (diff) | |
Make code more readable by not mixing list traversal and option processing.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions