From e79e501adaffafd4c76ffadd0f0cb4fbca3254a2 Mon Sep 17 00:00:00 2001
From: Joris van der Hoeven <vdhoeven@lix.polytechnique.fr>
Date: Thu, 12 Nov 2020 23:16:12 +0000
Subject: [PATCH] Attaching a favicon to an exported webpage

---
 main/convert/html/man-html.en.tm | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/main/convert/html/man-html.en.tm b/main/convert/html/man-html.en.tm
index f38572e..684657e 100644
--- a/main/convert/html/man-html.en.tm
+++ b/main/convert/html/man-html.en.tm
@@ -1,6 +1,6 @@
-<TeXmacs|1.99.9>
+<TeXmacs|1.99.15>
 
-<style|<tuple|tmdoc|english|old-spacing>>
+<style|<tuple|tmdoc|english|old-spacing|old-dots|old-lengths>>
 
 <\body>
   <tmdoc-title|Converters for <name|Html> and <name|MathML>>
@@ -52,6 +52,8 @@
 
     <item*|<src-var|html-head-javascript>>A <name|Javascript> script to be
     executed before the body.
+
+    <item*|<src-var|html-head-favicon>>A \Pfavicon\Q for your webpage.
   </description>
 
   You may also use the following macros:
@@ -115,7 +117,7 @@
 
   In the binary distributions, we have included <verbatim|wget>.
 
-  <tmdoc-copyright|1998--2019|Joris van der Hoeven>
+  <tmdoc-copyright|1998\U2019|Joris van der Hoeven>
 
   <tmdoc-license|Permission is granted to copy, distribute and/or modify this
   document under the terms of the GNU Free Documentation License, Version 1.1