Re: [PG-devel] defpacustom project-filename

2013-07-17 Thread Hendrik Tews
Hendrik Tews writes: I don't think using defpacustom for project-filename is a good idea. This way it appears in the menu and when you enable it, coq-project-filename is set to t. I fixed the t setting with fixing the :type of coq-project-filename. Now it can stay in the menu (although

[PG-devel] defpacustom project-filename

2013-07-17 Thread Hendrik Tews
Hi Pierre, I don't think using defpacustom for project-filename is a good idea. This way it appears in the menu and when you enable it, coq-project-filename is set to t. Can defpacustom handle string options, such that the user is queried for a string, when he enables the menu entry? Bye, Hend