<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <div class="moz-cite-prefix">Jonathan Fine wrote:<br>
      <br>
    </div>
    <blockquote type="cite"
cite="mid:CALD=Yf-iZSyarOB7nFdE4-4EsOGVV4Rc9xjeKQogm6n2H1k+Sg@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div>Philip wrote:</div>
        <br>
        <div class="gmail_quote">
          <blockquote class="gmail_quote" style="margin:0px 0px 0px
            0.8ex;border-left:1px solid
            rgb(204,204,204);padding-left:1ex">
            <div bgcolor="#FFFFFF">OK, we can know nothing of the
              preferences and opinions of those who create and support
              the production system</div>
          </blockquote>
          <div><br>
          </div>
          <div>I don't agree. We can simply ask the original poster.<br>
          </div>
          <div><br>
          </div>
          <blockquote class="gmail_quote" style="margin:0px 0px 0px
            0.8ex;border-left:1px solid
            rgb(204,204,204);padding-left:1ex">
            <div bgcolor="#FFFFFF">Again, we know only two things about
              the system.  It supports a file system, and it supports
              TeX.</div>
          </blockquote>
          <div><br>
          </div>
          <div>Again, I don't agree. We can simply ask the original
            poster.</div>
          <div><br>
          </div>
          <div>Once we have that information, we are better able to give
            advice and useful information. See also Mike's response to
            your earlier post.<br>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    Why not simply proceed on the basis of what we know, rather than
    waste the rest of eternity trying to establish exactly how many
    angels can sit on the head of a pin ?<br>
  </body>
</html>