PG icon indicating copy to clipboard operation
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`

Open JasonGross opened this issue 3 years ago • 1 comments

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')

JasonGross avatar Jun 30 '22 13:06 JasonGross

Since #590 was merged, using -arg -set -arg "'Loose Hint Behavior=Strict'" works. So this issue could be closed.

Columbus240 avatar Nov 06 '23 14:11 Columbus240