aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-07-25 11:53:43 +0200
committerPierre-Marie Pédrot2018-07-26 11:11:56 +0200
commit10d27ae6a016962173b0cc0ed6d2618a674e57aa (patch)
treee8b1653e6a5347b36c16df3138f7964da852c6e8
parentb13c954c49f546ecbbc5f73d32e69348408e2ad4 (diff)
Do not set diff printing on by default in CoqIDE.
-rw-r--r--ide/idetop.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 965bb913ff..854b1abe31 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -530,9 +530,6 @@ let () = Usage.add_to_usage "coqidetop"
let islave_init ~opts extra_args =
let args = parse extra_args in
CoqworkmgrApi.(init High);
- let open Coqargs in
- if not opts.diffs_set then
- Proof_diffs.write_diffs_option "on";
opts, args
let () =