diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-17 22:41:26 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-17 22:41:26 +0100 |
| commit | a91df5fdc60977accd7937eb17b62bd551d3213a (patch) | |
| tree | 982494df3d33609f5eb7c20b41211af1bb89995a /ide/coqide_ui.ml | |
| parent | 30076f81448721c49b86846de638cbc936c085fb (diff) | |
Remove Whelp commands.
Although these commands were never deprecated, they have been unusable for some
time now, since they send requests to an Italian server which is no longer
alive.
Diffstat (limited to 'ide/coqide_ui.ml')
| -rw-r--r-- | ide/coqide_ui.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index af71b1e78..edfe28b26 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -119,7 +119,6 @@ let init () = <menuitem action='About' /> <menuitem action='Locate' /> <menuitem action='Print Assumptions' /> - <menuitem action='Whelp Locate' /> </menu> <menu name='Tools' action='Tools'> <menuitem action='Comment' /> |