Am 24.09.2013 um 23:43 schrieb Makarius <[email protected]>: > 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?
It's probably important, but I don't use it (for lack of having memorized it). > 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. Cmd comma currently pops up an inline search. To me something like Alt Cmd F or Shift Cmd F would make sense, since it can be seen as a variation of Cmd F. Jasmin _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
