>    But admittedly, it also means that it's mostly useless as well: if your
>    Coq file is called ".v" the completion will stop at ".v" in any case,
> No, it won't, because Coq does also generate ".glob" files.

Indeed adding the .glob extension would be useful, contrary to the .vo
I was talking about.

> Additionally completion-ignored-extensions are hidden by default
> in dired buffers.

Not by default, no.  They are highlighted with a different face (the
face is `dired-ignored'), but you need to activate dired-omit for them
to be actually hidden.


        Stefan
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to