PG
PG copied to clipboard
Please support parsing `-arg -set -arg "Loose\ Hint\ Behavior=Strict"` and/or `-arg -set -arg "'Loose Hint Behavior=Strict'"` from `_CoqProject`
Currently, neither of these works with PG; the first gets passed as -set LooseHintBehavior=Strict, while the second gets passed as -set "'Loose" "Hint Behavior=Strict'", it seems (based on Don't know what to do with Hint Behavior=Strict')
Since #590 was merged, using -arg -set -arg "'Loose Hint Behavior=Strict'" works. So this issue could be closed.