diff options
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index cf54bfa2a..f8467f4f2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -134,7 +134,8 @@ let interp s = | VernacCheckMayEval _ | VernacGlobalCheck _ | VernacPrint _ - | VernacSearch _ -> () + | VernacSearch _ -> + !flash_info ~delay:1000000 "Warning: query commands should not be inserted in scripts" | _ -> () end; Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); |