svoid linux_fixNumPad() {
  if (!isLinux()) ret;
  sendToSuperUserVM("echo " + platformQuote(line) + " >>" + platformQuote(f));
  print("Fixed numpad for you! Please reboot machine for change to take effect.");
}