Only show the dynamic version menu in production environment where it's
available. Local (development) builds only show a stub version menu with
one item.
Also, fix the theme customization. Append version list items to the
correct element in html so that they are displayed correctly. Drop
unnecessary <div/>.
(cherry picked from commit 5295feb1ee)
Make it hidden, by default. Unify style with other items in the navbar
(making version list horizontal, for example). Show current version next
to the caret mark that opens the menu.
(cherry picked from commit e036d26953)
Make the list of available versions dynamic. The items displayed is now
generated with javascript. The parent directory of the site is supposed
to contain versions.js providing getVersionListItems() that returns the
available versions.
The update-gh-pages.sh script is modified to update/create versions.js
on every invocation. It simply lists all directories in the root
directory and adds them to the version list.
(cherry picked from commit c05c6f2e5b)
