diff options
| author | Maxime Dénès | 2016-04-12 18:59:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-04-12 19:05:30 +0200 |
| commit | 927e88de465e94bf18b970b45faaf97b4c2dff82 (patch) | |
| tree | 9519903aa6cf53dcb1de1958ecaf9b5045469738 /plugins/syntax/string_syntax.ml | |
| parent | 2bd36760f84f1d79af63cdee4d5d53f289a51204 (diff) | |
Quick fix for #4603 (part 2): Anomaly: Universe undefined
This is a follow-up on Matthieu's 7e7b5684
The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.
Thanks a lot to Enrico for his help!
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions