diff options
| author | Gaetan Gilbert | 2017-05-08 15:26:05 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-05-08 15:26:05 +0200 |
| commit | 75a808f893a68eaf82296535e0d168e0f09f8193 (patch) | |
| tree | b303fa172dbcb4501546e6051642c515567e59e3 /dev/include | |
| parent | e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 (diff) | |
Fix warnings in top_printers
Note that [@@@ocaml.warning "-32"] caused an error with Drop.
It was put there because I didn't realise the warning was about a real issue.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions