diff options
| author | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 15:36:20 +0100 |
|---|---|---|
| committer | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 15:57:52 +0100 |
| commit | fb0f3ff8c8e5a2e3b906dd9a8815a2d22ca9c38c (patch) | |
| tree | f99953c897acd0c2fabf75060e1845650547ccac /docs/_includes | |
| parent | 5d590242132b0f38fc04afed2c787dadfd8d6c2f (diff) | |
| download | dotty-fb0f3ff8c8e5a2e3b906dd9a8815a2d22ca9c38c.tar.gz dotty-fb0f3ff8c8e5a2e3b906dd9a8815a2d22ca9c38c.tar.bz2 dotty-fb0f3ff8c8e5a2e3b906dd9a8815a2d22ca9c38c.zip | |
Fix #1674: add search to doc site
Diffstat (limited to 'docs/_includes')
| -rw-r--r-- | docs/_includes/toc.html | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/docs/_includes/toc.html b/docs/_includes/toc.html index cac31d2bf..45cbb5940 100644 --- a/docs/_includes/toc.html +++ b/docs/_includes/toc.html @@ -4,6 +4,9 @@ {% include scala-logo.html %} </div> </a> + <form id="search-form" action="/search.html" method="get"> + <input placeholder="Search" type="text" id="search-box" name="query"> + </form> <ul id="categories"> <li><ul><li><a href="{{ site.baseurl }}/blog">Blog</a></li></ul></li> <li><ul><li><a href="{{ site.baseurl }}/docs">Dotty Docs</a></li></ul></li> |