diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-02 21:04:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-02 21:18:53 +0200 |
| commit | fd33e3875b872f8b83c350427a9809e68d7fe009 (patch) | |
| tree | 2744fbef32912950cf4dd698820296e477512584 /ide/wg_Find.mli | |
| parent | 04756f75bf54b1ccda8c180c62b14c5eaaaabb67 (diff) | |
Fixes #7636: location missing on deprecated compatibility notations.
Diffstat (limited to 'ide/wg_Find.mli')
0 files changed, 0 insertions, 0 deletions