message: Improve the formatting of shortcuts on macOS
diff: @@ -8,6 +8,8 @@ import { Logger, getLogger, log } from "extraterm-logging";
  import { KeybindingsFile, KeybindingsFileBinding } from './KeybindingsFile';
  import { Category } from '../ExtensionMetadata';
  +const isDarwin = process.platform === "darwin";
  +
  export interface KeyStrokeOptions {
  altKey: boolean;
  ctrlKey: boolean;
  @@ -59,16 +61,17 @@ export class KeyStroke {
  const parts: string[] = [];
  if (this.ctrlKey) {
  - parts.push("Ctrl");
  + parts.push(isDarwin ? "^" : "Ctrl");
  }
  if (this.metaKey) {
  parts.push("\u2318"); // Mac style 'pretzel' symbol
  }
  +
  if (this.altKey) {
  - parts.push("Alt");
  + parts.push(isDarwin ? "\u2325" : "Alt");
  }
  if (this.shiftKey) {
  - parts.push("Shift");
  + parts.push(isDarwin ? "\u21E7" : "Shift");
  }
  if (eventKeyToHumanMapping[this.configKey.toLowerCase()] !== undefined) {
  @@ -77,7 +80,7 @@ export class KeyStroke {
  parts.push(_.capitalize(this.configKey));
  }
  - this._humanReadableString = parts.join("+");
  + this._humanReadableString = parts.join(isDarwin ? "" : "+");
  return this._humanReadableString;
  }
  