Skip to content

Commit

Permalink
Update _base.html
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser authored and PatrickMassot committed May 1, 2022
1 parent 9b8778b commit 760b800
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion templates/_base.html
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@

<link rel="stylesheet" href="{{base_url}}/css/lean.css" >
<link rel="shortcut icon" href="{{base_url}}/img/favicon.ico">
<link rel="search" type="application/opensearchdescription+xml" title="mathlib docs" href="/opensearch.xml">
<link rel="search" type="application/opensearchdescription+xml" title="mathlib docs" href="{{base_url}}/opensearch.xml">
<link href="https://fonts.googleapis.com/css2?family=Merriweather&family=Open+Sans&family=Source+Code+Pro:wght@400;600&display=swap" rel="stylesheet">
{% block extracss %}{% endblock %}

Expand Down

0 comments on commit 760b800

Please sign in to comment.