src/tools/error_index_generator/error-index.js

   1 for (const elem of document.querySelectorAll("pre.playground")) {
   2     if (elem.querySelector(".compile_fail") === null) {
   3         continue;
   4     }
   5     const child = document.createElement("div");
   6     child.className = "tooltip";
   7     child.textContent = "ⓘ";
   8     elem.appendChild(child);
   9 }