diff options
| author | Jim Fehrle | 2019-11-04 19:14:07 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-11-06 11:24:27 -0800 |
| commit | db391451c5f89c034e6fec1b10fec66a25e3d4d4 (patch) | |
| tree | 49187070f11a607d08e2dad51da14cc823b863ef /kernel/nativevalues.ml | |
| parent | 634cb7b8a07a34fc29d074591091f0a6170f7bff (diff) | |
Replace "option" in doc when it refers to a flag
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions