* Changing hotkey in text editor for 'jumping' to a particular line to Ctrl-G, since this appears to be more standard (and is easier to hit).
* Changing hotkey in text editor for 'jumping' to a particular line to Ctrl-G, since this appears to be more standard (and is easier to hit).