From fc2683dd280bc6f39787de8e6a1be2110e64e75e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 3 Mar 2022 18:02:11 +0000 Subject: [PATCH 1/4] add search.xml --- templates/search.xml | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 templates/search.xml diff --git a/templates/search.xml b/templates/search.xml new file mode 100644 index 0000000000..b3a346a5de --- /dev/null +++ b/templates/search.xml @@ -0,0 +1,9 @@ + + mathlib + Search mathlib docs + UTF-8 + {{base_url}}/img/favicon.ico + + + {{base_url}}/mathlib_docs + From 6ca8efadace67017ce994c27884b88644afef28a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 3 Mar 2022 18:04:59 +0000 Subject: [PATCH 2/4] tidy --- templates/{search.xml => opensearch.xml} | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) rename templates/{search.xml => opensearch.xml} (68%) diff --git a/templates/search.xml b/templates/opensearch.xml similarity index 68% rename from templates/search.xml rename to templates/opensearch.xml index b3a346a5de..9d2702dbe2 100644 --- a/templates/search.xml +++ b/templates/opensearch.xml @@ -1,9 +1,8 @@ + mathlib Search mathlib docs UTF-8 {{base_url}}/img/favicon.ico - - {{base_url}}/mathlib_docs From 9924aa742545a5d81b12e2367972f1d7e311851d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 3 Mar 2022 18:05:32 +0000 Subject: [PATCH 3/4] Update _base.html --- templates/_base.html | 1 + 1 file changed, 1 insertion(+) diff --git a/templates/_base.html b/templates/_base.html index 5c70fc6a0e..5eeabd77c8 100644 --- a/templates/_base.html +++ b/templates/_base.html @@ -7,6 +7,7 @@ + {% block extracss %}{% endblock %} From f94d1b0a5bba66441293ae28bd974c001cd67ad9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 16 Mar 2022 14:14:36 +0000 Subject: [PATCH 4/4] Update _base.html --- templates/_base.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/_base.html b/templates/_base.html index 5eeabd77c8..0990523531 100644 --- a/templates/_base.html +++ b/templates/_base.html @@ -7,7 +7,7 @@ - + {% block extracss %}{% endblock %}