diff options
| author | Hugo Herbelin | 2018-09-20 12:59:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 13:28:36 +0200 |
| commit | f30996a89a31a1a54ab481f752e5febb8a8ac0ed (patch) | |
| tree | f6e0bfd3cabb85b486fe68a417ab7c2d3033a4b1 /kernel/nativelib.ml | |
| parent | 82a3fb5d5c0d0c5660effec59f3800ee5e8a125d (diff) | |
Fixing a typo in a comment.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions