} else if (keypress.equals(kbDel)) {
document.del();
alignCursor();
- } else if (keypress.equals(kbBackspace)) {
+ } else if (keypress.equals(kbBackspace)
+ || keypress.equals(kbBackspaceDel)
+ ) {
document.backspace();
alignTopLine(false);
} else if (keypress.equals(kbTab)) {
&& !keypress.getKey().isCtrl()
) {
// Plain old keystroke, process it
+ // TODO: fix document to use ints, not chars
document.addChar(keypress.getKey().getChar());
alignCursor();
} else {