From 7eb883b7c284c78cc17093bfc4ef2d70e0acad83 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ludovic=20Court=C3=A8s?= Date: Tue, 18 Jan 2022 22:20:12 +0100 Subject: [PATCH] doc: Add a language menu in the HTML manual. * doc/build.scm (stylized-html): New procedure. (html-manual): Use it. --- doc/build.scm | 156 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 153 insertions(+), 3 deletions(-) diff --git a/doc/build.scm b/doc/build.scm index 1057336c65..44c185e5f9 100644 --- a/doc/build.scm +++ b/doc/build.scm @@ -600,6 +600,154 @@ its
 blocks (as produced by 'makeinfo --html')."
 
   (computed-file name build))
 
+(define* (stylized-html source input
+                        #:key
+                        (languages %languages)
+                        (manual %manual)
+                        (manual-css-url "/static/base/css/manual.css"))
+  "Process all the HTML files in INPUT; add them MANUAL-CSS-URL as a