Merge branch 'main' into dev

1 files changed, 0 insertions, 12 deletions

diff --git a/docs/dev/articles/web_only/benchmarks_files/header-attrs-2.6/header-attrs.js b/docs/dev/articles/web_only/benchmarks_files/header-attrs-2.6/header-attrs.js
deleted file mode 100644
index dd57d92e..00000000
--- a/docs/dev/articles/web_only/benchmarks_files/header-attrs-2.6/header-attrs.js
+++ /dev/null
@@ -1,12 +0,0 @@
-// Pandoc 2.9 adds attributes on both header and div. We remove the former (to
-// be compatible with the behavior of Pandoc < 2.8).
-document.addEventListener('DOMContentLoaded', function(e) {
-  var hs = document.querySelectorAll("div.section[class*='level'] > :first-child");
-  var i, h, a;
-  for (i = 0; i < hs.length; i++) {
-    h = hs[i];
-    if (!/^h[1-6]$/i.test(h.tagName)) continue;  // it should be a header h1-h6
-    a = h.attributes;
-    while (a.length > 0) h.removeAttribute(a[0].name);
-  }
-});