diff options
| author | Pierre-Marie Pédrot | 2015-05-13 23:38:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-13 23:40:38 +0200 |
| commit | d91addb140ba7315d70c4599b0d058bef798ac1c (patch) | |
| tree | 9e4582ce5d8b7456fd7de6850941ee359d82fea4 /lib/flags.ml | |
| parent | 3a7095f9f6a09a4461c2124b0020dfe37962de26 (diff) | |
Fixing bug #4216:
Internal error: Anomaly: Uncaught exception Not_found. Please report.
An evarmap was lost because of an unsound typing primitive.
Diffstat (limited to 'lib/flags.ml')
0 files changed, 0 insertions, 0 deletions