diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-14 19:14:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-17 11:50:42 +0200 |
| commit | 6be0e422de395dbdeebb6c481511eb49945eeca8 (patch) | |
| tree | 32325bf3d51d907972f4099d6f77e3bb9f917379 /API | |
| parent | 41489a97014ab60b3dcc0f32dfdd10aacc6bcb98 (diff) | |
[funind] Remove spurious character in comment.
It breaks ocamlmerlin.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions