From 8e9042fa46e67f686de9b917c6dbcf49d585c38c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 15 Jun 2016 17:35:48 +0200
Subject: Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"

for uniformity with other Debug options.
---
 plugins/ssrmatching/ssrmatching.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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 }
-- 
cgit v1.2.3