diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 69cc0607b..b29bdf3f1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -495,7 +495,7 @@ let function_debug_sig = { optsync = false; optname = "Function debug"; - optkey = PrimaryTable("Function_debug"); + optkey = ["Function_debug"]; optread = (fun () -> !function_debug); optwrite = (fun b -> function_debug := b) } @@ -514,7 +514,7 @@ let strict_tcc_sig = { optsync = false; optname = "Raw Function Tcc"; - optkey = PrimaryTable("Function_raw_tcc"); + optkey = ["Function_raw_tcc"]; optread = (fun () -> !strict_tcc); optwrite = (fun b -> strict_tcc := b) } |