diff options
author | 2014-02-24 11:07:21 +0100 | |
---|---|---|
committer | 2014-02-24 11:07:21 +0100 | |
commit | c4370e5394cc9f678250150bd5bb407629b21913 (patch) | |
tree | aba0aac4e01f5ca2d5e0a6e2a82638fa65dc67bf /pretyping/recordops.mli | |
parent | 6b10edbe056f38d784258b6bf3ea4b8dc472e472 (diff) |
Fix grammatical mistake in error message (bug #3238)
Diffstat (limited to 'pretyping/recordops.mli')
0 files changed, 0 insertions, 0 deletions