Just FYI (in case you're not a watcher of ProofGeneral's GitHub repo), the change of PG's license to
GPL-3.0-or-later (undertook a couple of years ago, cf. #198) is now effective:
the corresponding PR #627 was just merged in master :relieved:
special thanks to @Stefan Monnier for his recent help on this topic!
So henceforth, PG has the very same license as that of GNU Emacs.
does PG's license affect users in any way? For example, can PG generate code under certain circumstances?
No (that's the reason why I posted this heads-up in
Proof General devs and not
Proof General users :)
Actually the only user-facing impact is for contributors:
beforehand, it was not possible to accept contributions that include-or-extend snippets directly taken from Emacs' codebase (because GPLv2 and GPLv3+ are incompatible).
Last updated: Feb 06 2023 at 07:03 UTC