aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ide_slave.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ide_slave.ml')
-rw-r--r--ide/ide_slave.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index aafc3fc59..5f40a2242 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -69,9 +69,7 @@ let ide_cmd_checks ~id (loc,ast) =
if is_known_option ast then
warn "Set this option from the IDE menu instead";
if is_navigation_vernac ast || is_undo ast then
- warn "Use IDE navigation instead";
- if is_query ast then
- warn "Query commands should not be inserted in scripts"
+ warn "Use IDE navigation instead"
(** Interpretation (cf. [Ide_intf.interp]) *)