468 function switch_lang(lang) {

   469     langnum = langs.indexOf(lang);

   470     if(langnum == -1) {

   471         console.log("Unknown language: "+lang+", return to original");

   472         location.reload(true);

   473     }

   474 

   475     for (let translation of translations) {

   476         let [objs, msgs] = translation;

   477         let msg = msgs[langnum];

   478         for (let obj of objs) {

   479             msg.split('\\\\n').map((line,i) => {obj.children[i].textContent = line;});

   480         }

   481     }

   482 }