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