diff options
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 d763c33cb..af71b1e78 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -51,7 +51,6 @@ let init () = <menuitem action='Find' /> <menuitem action='Find Next' /> <menuitem action='Find Previous' /> - <menuitem action='Replace' /> <menuitem action='Complete Word' /> <separator /> <menuitem action='External editor' /> |