diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-13 14:36:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-13 14:36:18 +0100 |
| commit | dcb23edad4debc0f4856580910cb5eba00077006 (patch) | |
| tree | 85718e43abd3b791bd6de478196b39531db7230b /ide/ideutils.ml | |
| parent | dc9b65741dae1b2bf58394e26c9155dad2bf7591 (diff) | |
Better error message for nested module application.
Fixes #3809.
Diffstat (limited to 'ide/ideutils.ml')
0 files changed, 0 insertions, 0 deletions