diff options
| author | Théo Zimmermann | 2016-09-28 16:46:32 +0200 |
|---|---|---|
| committer | GitHub | 2016-09-28 16:46:32 +0200 |
| commit | 9b1c4576d89014d686bc10f13455a52de8d793bf (patch) | |
| tree | 0837f50a4053a7ab3167a2e66dcb9c0049a93695 | |
| parent | 4e93587fd83bab4ad5c158aa6b3c194e8a7a5551 (diff) | |
Make error message more helpful.
CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.
| -rw-r--r-- | ide/ide_slave.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 1f933fb8a5..239fc587ce 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -98,7 +98,7 @@ let coqide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then - msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + msg_warning (strbrk"This will not work. Use CoqIDE view menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then |