| // Localized user interface. | |
| var tr = { | |
| "off": "off", | |
| "on": "on", | |
| "syntax": "Syntax-Highlighting", | |
| "lineno": "Line-Numbers", | |
| "reset": "Reset Slide", | |
| "format": "Format Source Code", | |
| "kill": "Kill Program", | |
| "run": "Run", | |
| "toc": "Table of Contents", | |
| "prev": "Previous", | |
| "next": "Next", | |
| "waiting": "Waiting for remote server...", | |
| "errcomm": "Error communicating with remote server.", | |
| }; |