Custom Query (361 matches)

Hi,

the changeset 7913:9ebd4b14cadc committed on Oct 11 20:07:17 2010 +0200 breaks the cache. To reproduce, open the attached coq file and

1. do proof-process-buffer, which yields an error because there are two declarations peirce
2. change the first peirce into peirce_1 and do proof-process-buffer again. The error persists, because Proof General sent peirce instead of peirce_1 to the prover. Further the locked region ends in the middle of an identifier.

Bye,

Hendrik Tews

Hi,

this docstring mentions the callbacks init-cmd and interactive-input. These seem not to exist any more. It does not mention proof-shell-set-silent and proof-shell-clear-silent.

Bye,

Hendrik Tews

cd doc; make dvi therefore gives

make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" dvi make[1]: Entering directory `/home/tews/src/pg/doc' make[1]: * No rule to make target `dvi'. Stop. make[1]: Leaving directory `/home/tews/src/pg/doc' make: * [dvi] Error 2

If the dvi format is not supported any more I suggest to remove all occurrences of dvi from doc/Makefile and doc/Makefile.doc.

Hendrik