Stream: Coq users

Topic: What does `-quiet` do?

view this post on Zulip Ali Caglayan (Aug 09 2020 at 20:41):

What does the -quiet flag do? I've seen it mentioned in #6708 but there is no documentation on it that I could find.

view this post on Zulip Théo Zimmermann (Aug 11 2020 at 15:07):

It is mentioned in coqtop -help:

  -quiet          unset display of extra information (implies -w "-all")

view this post on Zulip Théo Zimmermann (Aug 11 2020 at 15:09):

According to the code, the -silent and -quiet command-line flags just set the Silent flag and disable all warnings.

Last updated: Sep 23 2023 at 15:01 UTC