- needed to position the dropdown content */
+.dropdown {
+ position: relative;
+ display: inline-block;
+}
+
+/* Dropdown Content (Hidden by Default) */
+.dropdown-content {
+ display: none;
+ position: absolute;
+ background-color: #f1f1f1;
+ min-width: 160px;
+ box-shadow: 0px 8px 16px 0px rgba(0,0,0,0.2);
+ z-index: 1;
+}
+
+/* Links inside the dropdown */
+.dropdown-content a {
+ color: black;
+ padding: 4px 6px;
+ text-decoration: none;
+ display: block;
+}
+
+/* Change color of dropdown links on hover */
+.dropdown-content a:hover {background-color: #ddd}
+
+/* Show the dropdown menu (use JS to add this class to the .dropdown-content container when the user clicks on the dropdown button) */
+.show {display:block;}
diff --git a/version.js b/version.js
new file mode 100644
index 00000000..3307f57a
--- /dev/null
+++ b/version.js
@@ -0,0 +1,52 @@
+const versions = {
+ "main": "v1.10.2-dev1+g4b4c680 (main)",
+ "v1.10.1": "v1.10.1 (latest)"
+};
+
+var scripts = document.getElementsByTagName("script"),
+scriptUrl = new URL(scripts[scripts.length-1].src);
+docUrl = new URL(document.URL);
+baseUrl = new URL(scriptUrl)
+baseUrl.pathname = baseUrl.pathname.split('/').slice(0,-1).join("/")
+
+function urlForVersion(url, version) {
+ url = new URL(url);
+ pathname = url.pathname.replace(baseUrl.pathname, "");
+ parts = pathname.split("/");
+ parts[1] = version;
+ url.pathname = baseUrl.pathname + parts.join("/");
+ return url
+}
+
+function writeVersionDropdown() {
+ currentVersion = document.currentScript.parentNode.innerText;
+ document.currentScript.parentNode.classList.add("dropdown");
+ document.currentScript.parentNode.innerText = "";
+ document.write(' '+currentVersion+'');
+ document.write('
');
+ for(var version in versions) {
+ var label = versions[version];
+ document.write(' '+label+'');
+ }
+ document.write('
');
+};
+
+/* When the user clicks on the button,
+toggle between hiding and showing the dropdown content */
+function myFunction() {
+ document.getElementById("myDropdown").classList.toggle("show");
+}
+
+// Close the dropdown menu if the user clicks outside of it
+window.onclick = function(event) {
+ if (!event.target.matches('.dropbtn')) {
+ var dropdowns = document.getElementsByClassName("dropdown-content");
+ var i;
+ for (i = 0; i < dropdowns.length; i++) {
+ var openDropdown = dropdowns[i];
+ if (openDropdown.classList.contains('show')) {
+ openDropdown.classList.remove('show');
+ }
+ }
+ }
+}