Hi,

I fixed #467 now such that the menu entries (including "Time
commands") do work. If you type "Time" on your own, you have to
use customize yourself, see ticket #467. I hope this is
sufficient for closing the bug.

Bye,

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

Reply via email to