this repo has no description
1window.onload = function () {
2 var to_link = document.getElementsByClassName("highlight-minizinc");
3 for (var i = 0; i<to_link.length; i++) {
4 if (to_link[i].hasAttribute('id')) {
5 var newH6 = document.createElement('p');
6 newH6.setAttribute('class','caption doc-link-caption');
7 var newTag = document.createElement('a');
8 newTag.setAttribute('href','#'+to_link[i].getAttribute('id'));
9 newTag.setAttribute('class','headerlink');
10 newTag.innerText = "¶";
11 newH6.appendChild(newTag);
12 to_link[i].parentNode.insertBefore(newH6, to_link[i]);
13 newH6.appendChild(to_link[i]);
14 }
15 }
16};