diff options
| author | Maxime Dénès | 2014-12-29 16:07:10 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-01-06 15:09:04 +0100 |
| commit | e6c2dc742732e0b2db83585b4099beb1f284143f (patch) | |
| tree | c5825c20c94765da6fac299ef1329de3a4f5b2fe /kernel/nativecode.mli | |
| parent | f1db73816e4bd463cc81f34ba7e35857694bfa25 (diff) | |
Rename ill-named "imports" field of safe_env into "required".
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions