The kludge of reverting the Pause prompt string is no longer needed

... when using user_settings.js (i.e. to switch command shells), the user's
text.<lang>.ini is re-loaded, thus reverting any changes (e.g. made when
loading another shell, like simple.bin).

Also, this was causing the translated Pause strings (from text.<lang>.ini)
to be lost.

exec/default.js

@@ -10,7 +10,6 @@ require("userdefs.js", "UFLAG_T");
 require("nodedefs.js", "NODE_MAIN");
 require("key_defs.js", "KEY_UP");
 require("gettext.js", "gettext");
-bbs.revert_text(bbs.text.Pause);
 load("termsetup.js");
 var shell = load({}, "shell_lib.js");