diff options
| author | Théo Zimmermann | 2017-08-17 15:35:49 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-08-17 15:35:49 +0200 |
| commit | 6de02170275e49e5f58a93eb5513d5eb8cb9aa38 (patch) | |
| tree | df997be5196651ba2e00910cd681576b36f147d0 /kernel/nativelib.mli | |
| parent | 9d8a4a92f75dfc5d831efff4554c28d623d0868f (diff) | |
Use the wording suggested by Gaetan.
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions