diff options
| author | Maxime Dénès | 2018-10-30 12:48:16 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-30 13:11:30 +0100 |
| commit | 1b35eebd0ac45233ec1714a4040eddedf0d656f5 (patch) | |
| tree | 6e3aef35bdada8ab2dd06df2b48a35bb4e059748 /kernel/nativecode.mli | |
| parent | 0f7462cc5f8676edaa6b7052edaad40e32fc8234 (diff) | |
Avoid passing dummy env to error printer
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions