[ cleanup ] More html structure

gallais · gallais · commit 1a942bfc06a4 · 2023-10-13T10:59:13.000+01:00
diff --git a/travis/landing-bottom.html b/travis/landing-bottom.html
@@ -0,0 +1,4 @@
+      </ul>
+    </div>
+  </body>
+</html>
diff --git a/travis/landing-top.html b/travis/landing-top.html
@@ -0,0 +1,19 @@
+<html>
+
+  <head>
+    <title>Documention for the Agda standard library</title>
+  </head>
+
+  <body>
+    <div id="container" style="width:75%; margin:auto">
+
+      <h1>Development versions</h1>
+
+      <ul>
+        <li><a href="master">master</a></li>
+        <li><a href="experimental">experimental</a></li>
+      </ul>
+
+      <h1>Released versions</h1>
+
+      <ul>
diff --git a/travis/landing.html b/travis/landing.html
diff --git a/travis/landing.sh b/travis/landing.sh
@@ -3,12 +3,14 @@ set -o pipefail
 
 rm html/index.html
 
+cat landing-top.html >> landing.html
+
 find html/ -name "index.html" \
   | grep -v "master\|experimental" \
   | sort -r \
   | sed 's|html/\([^\/]*\)/index.html|  <li><a href="\1">\1</a></li>|g' \
   >> landing.html
 
-echo "</ul>" >> landing.html
+cat landing-bottom.html >> landing.html
 
 mv landing.html html/index.html

-Original file line number
+Diff line change
@@ @@ -0,0 +1,4 @@ @@
 +      </ul>
 +    </div>
 +  </body>
 +</html>