[ptp-dev] Should we move photran-dev to ptp-dev?

[Jeffrey Overbey <overbey2@xxxxxxxxxxxx>]

Release time might be a good time to bring this up.

Since photran-dev is pretty low-volume, and some Photran-related discussions (e.g., related to builds and release engineering) are held on ptp-dev anyway, would it make sense to shut down the photran-dev list and use ptp-dev instead?

I don't particularly care either way; I just thought it might be helpful to consolidate this traffic in one place.  I've started asking new Photran developers to subscribe to ptp-dev anyway.  There are lots of important discussions on ptp-dev (and on the PTP monthly calls), and I usually don't think to copy those to photran-dev...

Jeff