I had hoped the maintainer would comment, but since he didn't, I merged it. On Jul 20, 2020, at 13:40, Ruben Di Battista wrote: > Ping! :) > > On Thu, Jul 2, 2020 at 8:34 PM Ruben Di Battista wrote: >> >> https://github.com/macports/macports-ports/pull/6924