diff options
| author | Maxime Dénès | 2017-08-17 16:23:32 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-17 16:23:32 +0200 |
| commit | 88226ad302d4c128173644fc9d992ada67ba6d9c (patch) | |
| tree | 767960aeab21ad6d8114b05836c2f8ab5b6aa6b8 /kernel/nativelib.ml | |
| parent | b6ebf2c50d940e174c1860d5853d15619b0537b0 (diff) | |
| parent | 7f3a7aa17cddfda15146117f7f8a6c40a91ab243 (diff) | |
Merge PR #974: Change section caption, improve some wording
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions