1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
{% extends "!layout.html" %}
{% block htmltitle %}
<link rel=“preconnect” href=“https://fonts.googleapis.com“ crossorigin>
<link rel=“preconnect” href=“https://fonts.gstatic.com” crossorigin>
{{ super() }}
{% endblock %}
{% block scripts %}
{{ super() }}
{# Override home link to point to MuJoCo homepage.
Ideally this would be done as part of the theme rather than in JS.
#}
<script>
document.addEventListener('DOMContentLoaded', (event) => {
let home_link = document.querySelector('a.icon');
{# Be extra safe and don't break the page if theme changes and querySelector can't match. #}
if (home_link) {
home_link.href="https://mujoco.org";
}
});
</script>
{% endblock %}
|
