docs: fix api docs search (#17820)

pull/17826/head
Erick Friis 8 months ago committed by GitHub
parent 47b1b7092d
commit 6e854ae371
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194

@ -5,7 +5,7 @@
<script type="text/javascript" src="{{ pathto('_static/doctools.js', 1) }}"></script> <script type="text/javascript" src="{{ pathto('_static/doctools.js', 1) }}"></script>
<script type="text/javascript" src="{{ pathto('_static/language_data.js', 1) }}"></script> <script type="text/javascript" src="{{ pathto('_static/language_data.js', 1) }}"></script>
<script type="text/javascript" src="{{ pathto('_static/searchtools.js', 1) }}"></script> <script type="text/javascript" src="{{ pathto('_static/searchtools.js', 1) }}"></script>
<!-- <script type="text/javascript" src="{{ pathto('_static/sphinx_highlight.js', 1) }}"></script> --> <script type="text/javascript" src="{{ pathto('_static/sphinx_highlight.js', 1) }}"></script>
<script type="text/javascript"> <script type="text/javascript">
$(document).ready(function() { $(document).ready(function() {
if (!Search.out) { if (!Search.out) {

Loading…
Cancel
Save