On Fri, Jul 23, 2021 at 03:39:25AM -0400, Jeff King wrote: > The question here is: should we continue to omit it from the html build, > since it does not render well (i.e., should we simply drop this patch). I think that's a nice way of putting it. Since the HTML rendering is terrible, let's just drop this patch and leave cleaning it up as #leftoverbits. Thanks, Taylor