I am also in favor of releasing this patch, as it doeas not seem ro break the users old configuration settings using coq-prog-args (does it?).
Bye, Pierre Courtieu 2011/9/9 Hendrik Tews <[email protected]>: > Tom Prince <[email protected]> writes: > > Make coq-load-path accept either strings (which are passed "-I" options) > or conses of strings (which are passed as "-R" options). > > Thanks a lot for your patch. This has been on my todo list, > however, I never looked at this point, because I don't use -R (yet). > > Before I commit your patch to the repository, I would like to > discuss the following two points: > > * Proof General 4.1 will be released shortly (hopefully). I don't > know if the policy permits commits with new minor features. > David, could you comment on this? > > Probably a fair portion of the Coq users would benefit from the > patch. The patch is very small and can be easily tested. > Therefore, I would be in favor of committing the patch, > although Proof General is already deeply frozen. > > * With the patch, coq-load-path covers the options -I and > -R ... -as ... With a minor change we will also get -R ... > However, -I ... -as ... would still be unsupported. > > Does anybody use -I ... -as ... ?? Does anybody has an opinion > about whether Coq Proof General should support -I ... -as ... ?? > > [The point here is not the implementation, which would be very > simple. The point is, if and how to encode -I ... -as ... in > coq-load-path.] > > > Note that Tom's patch does not apply cleanly to cvs head any > more. When reading the patch I spotted some errors in the > documentation strings, which I fixed a few minutes ago. > > Bye, > > Hendrik > _______________________________________________ > ProofGeneral-devel mailing list > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
