diff options
author | Théo Zimmermann <theo.zimmi@gmail.com> | 2016-09-28 16:46:32 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-09-28 16:46:32 +0200 |
commit | 9b1c4576d89014d686bc10f13455a52de8d793bf (patch) | |
tree | 0837f50a4053a7ab3167a2e66dcb9c0049a93695 /LICENSE | |
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.
Diffstat (limited to 'LICENSE')
0 files changed, 0 insertions, 0 deletions