- var innerdivname = randomString(5);
- document.getElementById(target_div).innerHTML = "<div id=\"" + innerdivname +
- "\"><i class=\"fas fa-spinner fa-spin\"></i> "
- + _("Loading messages from server, please wait") + "</div>" ;
+ original_text = document.getElementById(target_div).innerHTML; // in case we need to replace it after an error
+ document.getElementById(target_div).innerHTML =
+ "<i class=\"fas fa-spinner fa-spin\"></i> "
+ + _("Loading messages from server, please wait") ;