Rename environment variable controlling public docs build

2024-05-21 15:22:40 -04:00
parent 09c1228712
commit 902c61bf47
2 changed files with 3 additions and 3 deletions
--- a/docs/_theme/main.html
+++ b/docs/_theme/main.html
@@ -2,8 +2,8 @@

 {% block site_meta %}
  {{ super() }}
-  {# Disable search indexing unless we're building for ReadTheDocs #}
-  {% if not config.extra.readthedocs %}
+  {# Disable search indexing unless we're building for public consumption #}
+  {% if not config.extra.build_public %}
    <meta name="robots" content="noindex">
  {% endif %}
 {% endblock %}