Version 2.1: documentation, public API headers, and sample programs.

PiperOrigin-RevId: 403900419
2021-10-18 12:23:02 +01:00
commit 1f7eaae62e
96 changed files with 28272 additions and 0 deletions
@@ -0,0 +1,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 %}