<html>

  <head>

    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">

  </head>

  <body text="#000000" bgcolor="#FFFFFF">

    <div class="moz-cite-prefix">

      <div class="moz-cite-prefix">I just used ""reply/all", as I always

        do, Siep -- the message came to me via TeX Live, so went back

        there.<br>

        ** Phil.<br>

        --------<br>

      </div>

      <br>

      Siep Kroonenberg wrote:<br>

    </div>

    <blockquote type="cite" cite="mid:20200822135047.GB1252@bitmuis.nl">

      <pre wrap="">On Sat, Aug 22, 2020 at 02:40:54PM +0100, Philip Taylor wrote:

So you forwarded my answer to the interested parties, which I

forgot? If so, thank you for that.

</pre>

    </blockquote>

    <br>

  </body>

</html>