diff options
| author | Clément Pit-Claudel | 2019-02-19 12:52:04 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-02-19 12:52:04 -0500 |
| commit | c39482e63aacf47359d8f76c44c2d851c7cfb9a5 (patch) | |
| tree | b57047087583c8d991aed295bfee679bf54fd85a /doc/sphinx/practical-tools | |
| parent | c3cc72ccf586703ed009a8bdd5df8d40b0384ab2 (diff) | |
| parent | 499491f8efd3a02dacb64c779edc246510b1d35f (diff) | |
Merge PR #9501: Sphinx: fail when a command fails + other stuff
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 1b4d2315aa..eebf1f11e1 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -34,6 +34,11 @@ allow dynamic linking of tactics). You can switch to the OCaml toplevel with the command ``Drop.``, and come back to the |Coq| toplevel with the command ``Coqloop.loop();;``. +.. flag:: Coqtop Exit On Error + + This option, off by default, causes coqtop to exit with status code + ``1`` if a command produces an error instead of recovering from it. + Batch compilation (coqc) ------------------------ |