From 339d2d5be0f924e4f5d093577f171158ef41be73 Mon Sep 17 00:00:00 2001
From: flip1995 <uwdkn@student.kit.edu>
Date: Mon, 19 Feb 2018 16:30:19 +0100
Subject: [PATCH] Fix name of configuration parameters in documentation

---
 util/lintlib.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/util/lintlib.py b/util/lintlib.py
index c46706352..190bce5e2 100644
--- a/util/lintlib.py
+++ b/util/lintlib.py
@@ -77,7 +77,7 @@ def parse_configs(path):
     confvars = re.findall(confvar_re, match.group(1))
 
     for (lint, doc, name, default, ty) in confvars:
-        configs[lint.lower()] = Config(name, ty, doc, default)
+        configs[lint.lower()] = Config(name.replace("_", "-"), ty, doc, default)
 
     return configs