Prepend "(DEV)" to HTML titles if build locally/not on RTD

(cherry picked from commit 0b6d26e33d7955590f1d75a816caff8cde251c42)

_templates/layout.html

@@ -12,3 +12,7 @@
   {% endif -%}
   {{ super() }}
 {% endblock -%}
+
+{% block htmltitle -%}
+<title>{{ godot_title_prefix }}{{ title|striptags|e }}{{ titlesuffix }}</title>
+{% endblock -%}

conf.py

@@ -128,6 +128,9 @@ html_context = {
     "godot_docs_suffix": ".html",
     "godot_default_lang": "en",
     "godot_canonical_version": "stable",
+    # Distinguish local development website from production website.
+    # This prevents people from looking for changes on the production website after making local changes :)
+    "godot_title_prefix": "" if on_rtd else "(DEV) ",
 }
 
 html_logo = "img/docs_logo.png"