diff options
Diffstat (limited to 'src/tools/error_index_generator/error-index.js')
-rw-r--r-- | src/tools/error_index_generator/error-index.js | 9 |
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); +} |