... 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.