"Use project file" option does not work

[proofgeneral]

"Use project file" option does not work

[Matafou]

Hi, thanks for reporting.

Can you try reverting the buffer after setting the option please? The check
for coq project file is done when loading the file (unless this was changed
by Clément lately).
If it does not work it is a bug, if it works it is a (reasonnable) feature
wish that this option take effet immediately.

P.

2016-02-04 19:03 GMT+01:00 Vadim Zaliva [email protected]:

driectory structure like this

[vzaliva]

M-x revert buffer did the trick. But I think this is very non-intuitive for user. It is reasonable to expect that I need to restart already running Coq process (if any), but since it was not started yet it is not clear that one would need to reopen file to apply this option.

[Matafou]

Agreed. On my todo list.
P.

Le vendredi 5 février 2016, Vadim Zaliva [email protected] a
écrit :

M-x revert buffer did the trick. But I think this is very non-intuitive
for user. It is reasonable to expect that I need to restart already running
Coq process (if any), but since it was not started yet it is not clear that
one would need to reopen file to apply this option.

—
Reply to this email directly or view it on GitHub
#45 (comment).

[Matafou]

This is supposed to be fixed by @cpitclaudel. Can someine confirm?