Add doc/index.html to redirect <homepage>/doc to the title page of the manual

wilfwilson · wilfwilson · commit 103c03fe1dec · 2025-09-20T15:29:45.000+01:00
This means that if a user requests https://digraphs.github.io/Digraphs/doc/ (which I think is a natural-enough thing to want to do), then instead of getting a 404 error, they are instead automatically redirected to the title page of the manual, which is presumably what they wanted, anyway. Unless and until gap-system/GitHubPagesForGAP#25 is merged, or gap-actions/update-gh-pages#10 is addressed in a way that lets us keeps this file purely in our gh-pages branch, then I think the best way to manage this file is to keep it in the repository here. Whenever the ReleaseTools script/release action is run, the doc/ directory of the gh-pages branch is deleted, and so if we only kept this file in the gh-pages branch, it would get deleted each time we make a new release. However, the doc/ directory of the gh-pages branch is re-populated with (amongst other things) the html files of the doc/ directory of this repository. In particular, by having this file in the doc/ directory of this repo, this means that the file is retained in the gh-pages branch, even across different releases of the package and runs of the ReleaseTools script/release action.
diff --git a/doc/index.html b/doc/index.html
@@ -0,0 +1,9 @@
+<html>
+  <head>
+    <meta http-equiv="refresh" content="0; url=chap0_mj.html" />
+    <title>Digraphs package for GAP – The manual</title>
+  </head>
+  <body>
+    <a href="chap0_mj.html">Click to access the title page of the manual.</a>
+  </body>
+</html>
