Add new release branch to docs versions

[noissue]

(cherry picked from commit 03ef150)

.ci/scripts/create_release_branch.sh

@@ -23,6 +23,9 @@ git branch "${NEW_BRANCH}"
 # Clean changelog snippets.
 find CHANGES/ \( -name "*.feature" -o -name "*.bugfix" -o -name "*.doc" -o -name "*.translation" -o -name "*.devel" -o -name "*.misc" \) -exec git rm -f \{\} +
 
+# Add to version.txt
+sed -i -e "1 i \\${NEW_BRANCH}" docs/versions.txt
+
 bumpversion minor --commit --message $'Bump version to {new_version}\n\n[noissue]' --allow-dirty
 
 git push origin "${NEW_BRANCH}"

docs_theme/main.html

@@ -34,7 +34,7 @@
         {% if config.theme.version.endswith("dev") -%}
         version_select.value = "";
         {% else -%}
-        version_select.value = "{{ config.theme.version }}";
+        version_select.value = "{{ config.theme.version }}".match("[0-9]+\.[0-9]+")[0];
         {% endif -%}
         version_select.onchange = function(event) { window.location = "{{ prefix }}{{ '.'|url }}" + event.target.value };
       })