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 /library/libobject.mli | |
| parent | d98a590b0637ca50380d424ae638d001c79305b9 (diff) | |
Documenting the "only printing" notation flag.
Diffstat (limited to 'library/libobject.mli')
0 files changed, 0 insertions, 0 deletions