From bc3cabc4d58d9f64c0a6bbb7ee0a2a51ab199120 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 3 Mar 2022 18:08:44 +0000
Subject: [PATCH 1/5] Create opensearch.xml

---
 templates/opensearch.xml | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 templates/opensearch.xml

diff --git a/templates/opensearch.xml b/templates/opensearch.xml
new file mode 100644
index 0000000..dabf1a4
--- /dev/null
+++ b/templates/opensearch.xml
@@ -0,0 +1,8 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<OpenSearchDescription xmlns="http://a9.com/-/spec/opensearch/1.1/" xmlns:moz="http://www.mozilla.org/2006/browser/search/">
+  <ShortName>mathlib</ShortName>
+  <Description>Search mathlib docs</Description>
+  <InputEncoding>UTF-8</InputEncoding>
+  <Image width="16" height="16" type="image/x-icon">{{base_url}}/static/favicon.ico</Image>
+  <Url type="text/html" method="GET" template="{{base_url}}/find/{searchTerms}" />
+</OpenSearchDescription>

From 6e0ff78daab81b451c024957a8eec92bc158ea57 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 3 Mar 2022 18:09:29 +0000
Subject: [PATCH 2/5] Update base.j2

---
 templates/base.j2 | 1 +
 1 file changed, 1 insertion(+)

diff --git a/templates/base.j2 b/templates/base.j2
index 7694b32..c151ab5 100644
--- a/templates/base.j2
+++ b/templates/base.j2
@@ -5,6 +5,7 @@
     <link rel="stylesheet" href="{{ site_root }}pygments.css">
     <link rel="stylesheet" href="{{ site_root }}pygments-dark.css">
     <link rel="shortcut icon" href="{{ site_root }}favicon.ico">
+    <link rel="search" type="application/opensearchdescription+xml" title="mathlib docs" href="{{ site_root }}opensearch.xml">
     <title>{% block title %}{% endblock %} - mathlib docs</title>
     <meta charset="UTF-8">
     <meta name="viewport" content="width=device-width, initial-scale=1">

From 0ee2ba69bf047592ea24eccb5ccb527fe9cf3e14 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 3 Mar 2022 18:10:04 +0000
Subject: [PATCH 3/5] Update opensearch.xml

---
 templates/opensearch.xml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/templates/opensearch.xml b/templates/opensearch.xml
index dabf1a4..381c435 100644
--- a/templates/opensearch.xml
+++ b/templates/opensearch.xml
@@ -3,6 +3,6 @@
   <ShortName>mathlib</ShortName>
   <Description>Search mathlib docs</Description>
   <InputEncoding>UTF-8</InputEncoding>
-  <Image width="16" height="16" type="image/x-icon">{{base_url}}/static/favicon.ico</Image>
-  <Url type="text/html" method="GET" template="{{base_url}}/find/{searchTerms}" />
+  <Image width="16" height="16" type="image/x-icon">{{ site_root }}/static/favicon.ico</Image>
+  <Url type="text/html" method="GET" template="{{ site_root }}/find/{searchTerms}" />
 </OpenSearchDescription>

From 26f094dbff2a183094ae3365b9723f8b07a78818 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 3 Mar 2022 18:12:56 +0000
Subject: [PATCH 4/5] Update print_docs.py

---
 print_docs.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/print_docs.py b/print_docs.py
index c84d90e..9ccf9c0 100644
--- a/print_docs.py
+++ b/print_docs.py
@@ -655,6 +655,9 @@ def write_html_files(partition, loc_map, notes, mod_docs, instances, tactic_docs
   current_project = None
   current_filename = None
 
+  with open_outfile('opensearch.xml') as out:
+    out.write(env.get_template('opensearch.xml.j2').render())
+
 def write_site_map(partition):
   with open_outfile('sitemap.txt') as out:
     for filename in partition:

From f5d0175b9a192be1ce7a30c9cc03116fe7cbea1e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 3 Mar 2022 18:13:28 +0000
Subject: [PATCH 5/5] Rename opensearch.xml to opensearch.xml.j2

---
 templates/{opensearch.xml => opensearch.xml.j2} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename templates/{opensearch.xml => opensearch.xml.j2} (100%)

diff --git a/templates/opensearch.xml b/templates/opensearch.xml.j2
similarity index 100%
rename from templates/opensearch.xml
rename to templates/opensearch.xml.j2