
<html>

  <head>

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

  </head>

  <body>

    <div class="moz-cite-prefix">On 5/2/20 2:16 PM, Greg Hellings wrote:<br>

    </div>

    <blockquote type="cite"

cite="mid:CAHxvOVJ7b4VdJ0SMrEC+ao0gC7OB1gFsLEBCQXkUWkaePhxzaQ@mail.gmail.com">Including

      that in my patch.</blockquote>

    <font face="FreeSerif">I see that git supports deleting a tag. 

      (Never noticed that before.)  Are we good with doing git tag -d

      4.2.0, merging a patch, and re-tagging?</font><br>

  </body>

</html>