commit edde409f60d9190ac65a45475cb2f773a4a7da03
author Ezio Melotti <ezio.melotti@gmail.com> Sat Oct 27 23:13:22 2012 +0300
committer Ezio Melotti <ezio.melotti@gmail.com> Sat Oct 27 23:13:22 2012 +0300
tree 85049f7a94fcba4ead2883dc8c3937272adc0e14
parent fe71bb52e4e845524233103915b8890b3a9e5f01
parent e5b1023ae2d5c99a98e68c2b997452551d07fa2f

#8040: merge with 3.2.

Doc/tools/sphinxext/static/version_switch.js

diff --git a/Doc/tools/sphinxext/static/version_switch.js b/Doc/tools/sphinxext/static/version_switch.js
index cc99153..363bebf 100644
--- a/Doc/tools/sphinxext/static/version_switch.js
+++ b/Doc/tools/sphinxext/static/version_switch.js
@@ -52,8 +52,12 @@
   }
 
   $(document).ready(function() {
-    var select = build_select(DOCUMENTATION_OPTIONS.VERSION,
-                              DOCUMENTATION_OPTIONS.RELEASE);
+    var version = DOCUMENTATION_OPTIONS.VERSION.split('.'),
+        release = DOCUMENTATION_OPTIONS.RELEASE || DOCUMENTATION_OPTIONS.VERSION;
+
+    version = version[0] + '.' + version[1];
+    var select = build_select(version, release);
+
     $('.version_switcher_placeholder').html(select);
     $('.version_switcher_placeholder select').bind('change', on_switch);
   });