diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:21:35 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:21:35 +0200 |
| commit | bff880ffb6ef33c99a96e7925c995b31b1497e6a (patch) | |
| tree | 1648e77d2abfdbfc3bbc567472e3835042e2dd69 /ide | |
| parent | 367e1f913f8d0b921dc4902b83d889dac3576580 (diff) | |
| parent | c78af970e1f003587fba9bebdf3ab5ca3b23face (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'ide')
| -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 bb8723dfe..5b07d3ec3 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -100,7 +100,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 - Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then |