diff options
| author | Pierre-Marie Pédrot | 2014-09-21 19:03:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-21 19:03:14 +0200 |
| commit | a30a8f484a478e04a7a42526cd6994310c59521d (patch) | |
| tree | 11bc0fc3d6dd50f6de8343df0986f0ace1cb85fc /kernel/nativecode.mli | |
| parent | e8726550e01e51ef3ccf8602f2ecbe2b3737cca3 (diff) | |
Removing a nonsensical Errors.push.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions