aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 2d7dd9d6c7..418980c54b 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -31,7 +31,7 @@ let _=
let gdopt=
{ optsync=true;
optname="Congruence Verbose";
- optkey=SecondaryTable("Congruence","Verbose");
+ optkey=["Congruence";"Verbose"];
optread=(fun ()-> !cc_verbose);
optwrite=(fun b -> cc_verbose := b)}
in