Simon Hudon (May 24 2022 at 23:19): Simon Hudon (May 24 2022 at 23:19):I wrote a patch to allow users to change the way goals get recentered after they get displayed. I'd like to upstream it. Should I just create a pull request on the PG repo?
Notification Bot (May 25 2022 at 05:59):This topic was moved to #Proof General devs > Pull Requests by Karl Palmskog.
Last updated: Feb 06 2023 at 07:03 UTC