PG gets confused by comment in _CoqProject file that involves "-arg"

[RalfJung]

I have this in my _CoqProject file:

#-arg -w -arg -notation-incompatible-prefix

I have this because I want to temporarily disable this flag to see where exactly the warning gets triggered.

However, this seems to confuse PG. I now get errors when starting Coq:

Don't know what to do with -notation-incompatible-prefix
See -help for the list of supported options

It seems like PG is passing -notation-incompatible-prefix, i.e. the 2nd of the two arguments in the above comment, to Coq. However this doesn't make a lot of sense since the entire line is commented out! I would expect none of the two arguments to be passed.

When this _CoqProject is passed to coq_makefile, things work as expected.

[hendriktews]

Thanks for the report. IMO we should fix this, because the Coq refman says that _CoqProject may contain "Comments, started with an unquoted # and continuing to the end of the line." and also that "# outside of double quotes starts a comment that continues to the end of the line. Comments are ignored."