redirect docs/ to docs/latest

brownplt · May 22, 2023 · 0c4c2ee · 0c4c2ee
1 parent aed5de5
commit 0c4c2ee
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 1 deletion.
diff --git a/Makefile b/Makefile
@@ -22,14 +22,18 @@ docs/latest:
 	mkdir -p site/docs/
 	cp -r latest-docs/build/docs site/docs/latest
 
+site/docs/index.html:
+	mkdir -p site/docs/
+	cp src/docs-redirect.html site/docs/index.html
+
 CM_JS = site/js/codemirror.js site/js/pyret.js site/js/runmode.js
 
 .Phony: pages
 pages: $(CM_JS)
 	raco frog -b
 
 .Phony: pages-and-docs
-pages-and-docs: pages docs/horizon docs/latest
+pages-and-docs: pages docs/horizon docs/latest site/docs/index.html
 
 .Phony: serve
 serve:

diff --git a/src/docs-redirect.html b/src/docs-redirect.html
@@ -0,0 +1,9 @@
+<!DOCTYPE html>
+<html>
+  <head>
+    <meta http-equiv="refresh" content="0; url='/docs/latest/" />
+  </head>
+  <body>
+    <p>Redirecting to the latest docs, or go directly to <a href="/docs/latest">/docs/latest/</a>.
+  </body>
+</html>