Change .gitignore; push docs/build to GitHub

2024-01-23 17:16:12 +01:00
parent 91b10cc90a
commit 4b862185e6
130 changed files with 27380 additions and 0 deletions
@@ -115,3 +115,7 @@ MUJOCO_LOG.TXT

 # vscode
 .vscode
+
+# Push HTML of docs to GitHub
+# Could be solved via a GitHub Action instead in the future, but that would use up compute for ALRhub
+!docs/build/