+function copy_to_clipboard(id)
+{
+ const tmp = document.createElement("input");
+ tmp.setAttribute("value", document.getElementById(id).innerHTML);
+ document.body.appendChild(tmp);
+ tmp.select();
+ document.execCommand("copy");
+ document.body.removeChild(tmp);
+}
+