1 files changed, 9 insertions, 0 deletions
diff --git a/src/tools/error_index_generator/error-index.js b/src/tools/error_index_generator/error-index.js
new file mode 100644
index 000000000..39b371be0
--- /dev/null
+++ b/src/tools/error_index_generator/error-index.js
@@ -0,0 +1,9 @@
+for (const elem of document.querySelectorAll("pre.playground")) {
+    if (elem.querySelector(".compile_fail") === null) {
+        continue;
+    }
+    const child = document.createElement("div");
+    child.className = "tooltip";
+    child.textContent = "ⓘ";
+    elem.appendChild(child);
+}