Stream: Coq devs & plugin devs

Topic: -set option true/false ===< yes/no?

view this post on Zulip Pierre Courtieu (Apr 01 2021 at 19:37):

Hi there!
In master the -set "XXX=true" is not accepted anymore. But in v8.13 `-set "XXX=yes" is not accepted. Is it on purpose?

view this post on Zulip Théo Zimmermann (Apr 01 2021 at 19:46):

Hum, I'm surprised to hear that!

view this post on Zulip Enrico Tassi (Apr 01 2021 at 19:53):

Maybe there is bug, but in the PRs we agreed to accept "yes" and "true" as synonyms IIRC. So it is not on purpose...

Last updated: May 28 2023 at 13:30 UTC