aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorEnrico Tassi2016-06-15 17:35:48 +0200
committerEnrico Tassi2016-06-15 17:35:48 +0200
commit8e9042fa46e67f686de9b917c6dbcf49d585c38c (patch)
treebd51a942d616b0642692a9ed575a23de0b664ce8 /plugins
parent1c52fa242b4584401939ebdc61f1acafff40d2de (diff)
Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"
for uniformity with other Debug options.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index b25f0f2341..718296c501 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -71,7 +71,7 @@ let _ =
Goptions.declare_bool_option
{ Goptions.optsync = false;
Goptions.optname = "ssrmatching debugging";
- Goptions.optkey = ["SsrMatchingDebug"];
+ Goptions.optkey = ["Debug";"SsrMatching"];
Goptions.optdepr = false;
Goptions.optread = (fun _ -> !pp_ref == ssr_pp);
Goptions.optwrite = debug }