diff --git a/doc/source/_static/pop_ver.js b/doc/source/_static/pop_ver.js new file mode 100644 index 0000000000..b8c58658a8 --- /dev/null +++ b/doc/source/_static/pop_ver.js @@ -0,0 +1,37 @@ +$(document).ready(function() { + /* For a URL that looks like + https://blah.github.io/versions/VERSIONFOO/html/bar/index.html, set cur_version_dir to + 'VERSIONFOO' (i.e., the portion of the path following 'versions'). + */ + var proj_end = document.baseURI.indexOf("versions") + 9; + var end = document.baseURI.indexOf("/", proj_end); + var cur_version_dir = document.baseURI.substring(proj_end, end); + var mylist = $("#version-list"); + mylist.empty(); + $.getJSON(version_json_loc, function(data) { + if (data.hasOwnProperty(cur_version_dir)) { + /* First add the current version so that it appears first in the drop-down + menu and starts as the selected element of the menu. If you click on the + current version, you should stay at the current page. + + The conditional around this block should generally be true, but we check it + just in case the current version is missing from the versions.json file for + some reason. + */ + cur_version_name = data[cur_version_dir]; + mylist.append($("