// On Linux Mint: Go to Keyboard settings instead, then Layouts / Options / Misc compatibility options => check "Num lock on: digits; ..."
svoid linux_fixNumPad() {
  if (!isLinux()) ret;
  File f = newFile("/etc/default/keyboard");
  S line = "XKBOPTIONS=\"numpad:microsoft\"";
  S cmd = "echo " + platformQuote(line) + " >>" + platformQuote(f);
  File cmdFile = javaxCachesDir("numpad.sh");
  saveTextFile(cmdFile, cmd);
  makeExecutable(cmdFile);
  backtickInSuperUserVM(platformQuote(cmdFile), true);
  print("Fixed numpad for you (hopefully)! Please reboot machine for change to take effect.");
}