aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2021-01-06 18:21:55 +0100
committerEnrico Tassi2021-01-27 09:45:49 +0100
commitd414273bbd53681baecf3ddc6d343243c80e8103 (patch)
tree190a40cbc6f423865bc14bed8f471b6bc4014fd8
parent0a531fae53c31ef76ff25fbfd3ceb8b5b33aa264 (diff)
[coqargs] use standard option injection for -print-emacs
-rw-r--r--sysinit/coqargs.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index faa26423e5..c4f12f6bb7 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -172,7 +172,7 @@ let add_set_option opts opt_name value =
(** Options for proof general *)
let set_emacs opts =
- Goptions.set_bool_option_value Printer.print_goal_tag_opt_name true;
+ let opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in
{ opts with config = { opts.config with print_emacs = true }}
let set_logic f oval =