diff options
| author | Hugo Herbelin | 2015-12-05 10:28:09 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 10:28:09 +0100 |
| commit | 3a29016f5b73815454ce8d9a74a017857e926706 (patch) | |
| tree | e7d22e8376cf1fc63b53d01b2110cddba75c33cb /dev/include | |
| parent | b7e72d0e0ca64168fc16875bf779dbc27d2a1820 (diff) | |
Fixing compilation of mli documentation.
Using dummy comment to @raise to please ocamldoc. Please change MS or
PMP, if needed.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions