diff options
author | 2015-12-05 10:28:09 +0100 | |
---|---|---|
committer | 2015-12-05 10:28:09 +0100 | |
commit | 3a29016f5b73815454ce8d9a74a017857e926706 (patch) | |
tree | e7d22e8376cf1fc63b53d01b2110cddba75c33cb /Makefile.build | |
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 'Makefile.build')
0 files changed, 0 insertions, 0 deletions