is the bug mentioned in https://github.com/coq/coq/commit/870d81c699b5d15420a03f2006a7938a158c09a8 reopened?
It depends if the load paths are now part of the summary or not (at that time, they were not)
I believe they should, otherwise
Undo has no effect on that command
but we link plugins before we unfreeze the normal summaries so how does it matter if the loadpath is in the summary?
Right, so one more reason to ditch Add LoadPath
Last updated: Nov 29 2023 at 18:01 UTC