1 //--- list of versions ---
3 "main": "11.2.0-dev16",
8 //--- list of versions ---
10 var script = document.currentScript
11 if (script && script.src) {
12 var scriptUrl = new URL(script.src);
13 var docUrl = new URL(document.URL);
14 var baseUrl = new URL(scriptUrl)
15 baseUrl.pathname = baseUrl.pathname.split('/').slice(0,-1).join("/")
17 function urlForVersion(url, version) {
19 pathname = url.pathname.replace(baseUrl.pathname, "");
20 parts = pathname.split("/");
22 url.pathname = baseUrl.pathname + parts.join("/");
26 function writeVersionDropdown() {
27 currentVersion = document.currentScript.parentNode.innerText;
28 document.currentScript.parentNode.classList.add("dropdown");
29 document.currentScript.parentNode.innerText = "";
30 document.write(' <span onclick="myFunction()" class="dropbtn">'+currentVersion+'</span>');
31 document.write(' <div id="myDropdown" class="dropdown-content">');
32 for(var version in versions) {
33 var label = versions[version];
34 if (label != version) {
35 label += " ("+version+")"
37 label = "Version " + label
38 document.write(' <a href="'+urlForVersion(docUrl, version)+'">'+label+'</a>');
40 document.write(' </div>');
43 function writeVersionDropdown() {}
46 /* When the user clicks on the button,
47 toggle between hiding and showing the dropdown content */
48 function myFunction() {
49 document.getElementById("myDropdown").classList.toggle("show");
52 // Close the dropdown menu if the user clicks outside of it
53 window.onclick = function(event) {
54 if (!event.target.matches('.dropbtn')) {
55 var dropdowns = document.getElementsByClassName("dropdown-content");
57 for (i = 0; i < dropdowns.length; i++) {
58 var openDropdown = dropdowns[i];
59 if (openDropdown.classList.contains('show')) {
60 openDropdown.classList.remove('show');