8c22181156
PiperOrigin-RevId: 720232771 Change-Id: I176db4d4168c37b2819df14b439c4cde838e2025
22 lines
757 B
HTML
22 lines
757 B
HTML
{% 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 homeLink = document.querySelector('a.icon');
|
|
{# Be extra safe and don't break the page if theme changes and querySelector can't match. #}
|
|
if (homeLink) {
|
|
homeLink.href="https://mujoco.org";
|
|
}
|
|
});
|
|
</script>
|
|
{% endblock %}
|