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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
