From 2c286519b3442e64fa049ef4b8b797bb550e624c Mon Sep 17 00:00:00 2001
From: Max Hilbrunner <m.hilbrunner@gmail.com>
Date: Mon, 27 Apr 2020 20:00:25 +0200
Subject: [PATCH] Prepend "(DEV)" to HTML titles if build locally/not on RTD

(cherry picked from commit 0b6d26e33d7955590f1d75a816caff8cde251c42)
---
 _templates/layout.html | 4 ++++
 conf.py                | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/_templates/layout.html b/_templates/layout.html
index 84503df34..6a55c539a 100644
--- a/_templates/layout.html
+++ b/_templates/layout.html
@@ -12,3 +12,7 @@
   {% endif -%}
   {{ super() }}
 {% endblock -%}
+
+{% block htmltitle -%}
+<title>{{ godot_title_prefix }}{{ title|striptags|e }}{{ titlesuffix }}</title>
+{% endblock -%}
diff --git a/conf.py b/conf.py
index 06aca56ae..a3e052635 100644
--- a/conf.py
+++ b/conf.py
@@ -116,6 +116,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"