diff options
| author | Emilio Jesus Gallego Arias | 2019-03-20 02:21:14 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-20 02:21:14 +0100 |
| commit | e5a2f0452cf9523bc86e71ae6d2ac30883a28be6 (patch) | |
| tree | 91492ff7e20a3ad53c42257e04e0a0f44909ed42 /toplevel | |
| parent | 9681f4bd4e184e3d748c4539667460537b55429f (diff) | |
| parent | ef2fce93057484b015c85713ad83f53f88762271 (diff) | |
Merge PR #8669: Show diffs in some error messages
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jfehrle
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f7fb26fe3a..626023737b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -94,9 +94,12 @@ let init_color opts = | Some "" -> false (* No color output *) | Some s -> Topfmt.parse_color_config s; true (* Overwrite all colors *) end - else - false + else begin + Topfmt.default_styles (); false (* textual markers, no color *) + end in + if not term_color then + Proof_diffs.write_color_enabled term_color; if Proof_diffs.show_diffs () && not term_color then (prerr_endline "Error: -diffs requires enabling -color"; exit 1); Topfmt.init_terminal_output ~color:term_color |