diff options
| author | Pierre-Marie Pédrot | 2016-06-28 01:10:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-28 01:19:46 +0200 |
| commit | ee0d4870fb982877be7cf07c75e3d039b82ddfc0 (patch) | |
| tree | c3c266d03e5c680bfee31011d57a74634fde0dfc /kernel/nativelib.ml | |
| parent | d98a590b0637ca50380d424ae638d001c79305b9 (diff) | |
Documenting the "only printing" notation flag.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions