diff options
| author | Jason Gross | 2017-06-07 15:54:37 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-06-15 16:37:56 -0400 |
| commit | 15d61838d7435b45559d648bcde1ccfb6e468bcd (patch) | |
| tree | 295aba6e5c5403814bf7859c120c608851e0ebe0 /kernel/nativecode.mli | |
| parent | da62d0dd86fc140ff58d9366a7a85e9b21b104b9 (diff) | |
Fix `make TIMED=1` garbage
It should not emit ` (user: 0.00 mem: 2852 ko)` multiple times
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions