#128 Tool settings are broken

[Anonymous]

"I selected the tools that output to DVI, which I don't use, and pressed delete but instead it deleted another tool. I didn't see this immediately and pressed delete again, which means I just deleted two of the three tools I wanted to keep: to output to a pdf in a single window and in split view. However, I can't add them back because the "new" button doesn't do anything."