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 <t...@os.inf.tu-dresden.de>:
> Tom Prince <tom.pri...@ualberta.net> 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
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to