<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    Hi Johannes,<br>
    <br>
    <div class="moz-cite-prefix">On 17.02.22 11:45, Johannes Heck wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CACQ49LnZ8X4BBCfz7R-oH3mMnzGUiK66ft4tH7VGc1Tc=TdNJA@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div class="gmail_quote">I've just installed the nightly, some
          first impressions:<br>
        </div>
      </div>
    </blockquote>
    <br>
    Thanks for testing.<br>
    <br>
    <blockquote type="cite"
cite="mid:CACQ49LnZ8X4BBCfz7R-oH3mMnzGUiK66ft4tH7VGc1Tc=TdNJA@mail.gmail.com">
      <div dir="ltr">
        <div class="gmail_quote">
          <div dir="ltr">
            <div>I like the new default syntax highlighting (I've been
              using MiKTex's version before, my highlighting was
              different somehow).</div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    Great.<br>
    <br>
    <blockquote type="cite"
cite="mid:CACQ49LnZ8X4BBCfz7R-oH3mMnzGUiK66ft4tH7VGc1Tc=TdNJA@mail.gmail.com">
      <div dir="ltr">
        <div class="gmail_quote">
          <div dir="ltr">
            <div>I also like the new draggable ruler, but: I miss a
              changing mouse pointer when hovering the ruler, so that
              it's obvious that there is something draggable hidden, the
              "hand" pointer e.g.</div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    I'll look into it. Maybe it would be beneficial to use the same
    cursor you get when hovering over an existing guideline, for the
    sake of consistency (although this is slightly more difficult to
    implement)...<br>
    <br>
    <blockquote type="cite"
cite="mid:CACQ49LnZ8X4BBCfz7R-oH3mMnzGUiK66ft4tH7VGc1Tc=TdNJA@mail.gmail.com">
      <div dir="ltr">
        <div class="gmail_quote">
          <div dir="ltr">
            <div>Another point is: on my ruler, the zero-point is
              captioned with "2.22045e-16". Is this an insider joke or
              an Bug? Why isn't it just "0"?</div>
          </div>
        </div>
      </div>
    </blockquote>
    <br>
    This would be a bug (most likely stemming from imprecise floating
    point numbers and the conversion from page coordinates to screen
    coordinates).<br>
    What operating system are you using (as for me on Ubuntu Linux,
    typically 0 is displayed).<br>
    <br>
    Best,<br>
    Stefan<br>
  </body>
</html>