On Mon, 12 Sep 2011 08:06:23 +0200, Hendrik Tews <[email protected]> wrote: > Tom Prince <[email protected]> writes: >> Does anybody use -I ... -as ... ?? Does anybody has an opinion >> about whether Coq Proof General should support -I ... -as ... ?? > > I suspect that it isn't worth it. If there are no subdirectories, > -R ... ... and -I ... -as ... have the same effect. > > Sure, but if there are subdirectories, the effect is different.
Unless somebody else chimes in I would say we shouldn't bother. If somebody has hierarchy of coq directories, to give an explicit name to one, I can't imagine that they wouldn't want the directory hierarchy reflected in the coq hierarchy. If somebody needs it later, we can always add it. On Mon, 12 Sep 2011 08:01:35 +0200, Hendrik Tews <[email protected]> wrote: > > 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?). > > No, as long as coq-compile-before-require is nil. It actually only affected me (and seemed to work) with coq-compile-before-require was t. _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
