diff options
| author | Pierre-Marie Pédrot | 2016-10-02 01:42:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-02 01:42:29 +0200 |
| commit | 109e05059692d0f2f15a4b1699ff4a25d07e5a79 (patch) | |
| tree | 4cc5a8a736fcbe978ca990f0b1a61143e594d1cd /kernel/nativecode.ml | |
| parent | acbe712fd643516ff63ecfe3e106deb695dbd9b3 (diff) | |
Fix bug #5087: Improve the error message on record with duplicated fields.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions