diff options
| author | Emilio Jesus Gallego Arias | 2017-04-21 15:01:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-21 15:04:56 +0200 |
| commit | e1637bef0f38b46840f146f146ddd4f17bec129a (patch) | |
| tree | f3e578d92f0896aee8b7482b00a9072a88e73eeb /plugins/syntax/string_syntax.ml | |
| parent | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff) | |
[ide] Fix #5482 "location for query commands" in IDE.
This warning is a special case as it happens outside the execution
context.
We could move the check inside, but instead we opt for the simpler
solution of properly setting the warning target.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions