<div dir="ltr"><div>I&#39;m good with it. Typically things pushed publicly you&#39;re discouraged from modifying, but I see no issues in this case.</div><div><br></div><div>--Greg<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, May 2, 2020 at 1:18 PM Karl Kleinpaste &lt;<a href="mailto:karl@kleinpaste.org">karl@kleinpaste.org</a>&gt; wrote:<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>
    <div>On 5/2/20 2:16 PM, Greg Hellings wrote:<br>
    </div>
    <blockquote type="cite">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>
  </div>

</blockquote></div>