Feature #136
GUI: Add an edit menu to the top bar (CoCoA GUI on MacOS)
Start date:
23 Apr 2012
Due date:
% Done:
0%
Estimated time:
Description
Mac users expect to find drop down menus on the top menu bar.
CoCoA GUI offers no such menu for editing commands (such as "undo").
Defect reported by Robbiano.
History
#1
Updated by Anna Maria Bigatti about 10 years ago
Updated by - Target version set to CoCoA-5.1.0 Easter14
#2
Updated by John Abbott about 10 years ago
Updated by - Target version changed from CoCoA-5.1.0 Easter14 to CoCoA-5.1.1 Seoul14
#3
Updated by Anna Maria Bigatti almost 10 years ago
- Subject changed from Add an edit menu to the top bar (CoCoA GUI on MacOS) to GUI: Add an edit menu to the top bar (CoCoA GUI on MacOS)
- Target version changed from CoCoA-5.1.1 Seoul14 to CoCoA-5.?.?