[isabelle-dev] Preferences on Mac OS X

[Makarius]

This is a question to hard-core users of Mac OS X.

How important is the canonical key sequence "COMMAND comma" as defined by 
Apple?

See also 
http://sourceforge.net/tracker/?func=detail&aid=3615047&group_id=588&atid=100588

For me as multiplatform user, it is more annoying to have different ways 
to do the same thing.  C+comma is quite central in jEdit, so my own 
tendency would be to find a way to take it away from Apple, not the other 
way round.

Alternatively, I am open to suggestions for a replacement key for the 
default keymap, one that works on English, German, French keyboards, or 
lets say 2 out of these 3.


 	Makarius