What is the problem here? Coq outputting the warning _after_ the
error? Or matching the warning as urgent message? Or searching
for errors only behind urgent messages?
From Proof General's point of view, the first of these is the problem,
since the behaviour has been well specified for a long t
Hello Hendrik,
It is a good idea to add a note to the trac. I would say that the
support is currently by best efforts of people who have other jobs and
little spare time -- such as you and I.
I think there are other people on this list but probably no very active
developers at the moment.
Hi,
currently, proof-shell-filter looks for urgent messages before
looking for errors. Moreover, if an urgent message is found, it
searches for errors only in the output that follows the urgent
message.
This behavior is responsible for issue #463, where Coq outputs an
error before a warning and
Hi,
do we have a support problem for Proof General?
I am asking because we have issues in the tracker that are quite
old and nobody seems to care... for instance #460 or #463 to
which I gave partial answers today.
Do we have a lack of developers or do the developers not like to
comment on issues