From b46a3e53240bd09b67e99b9db859cf797758cdf6 Mon Sep 17 00:00:00 2001 From: Pascal Hertleif Date: Tue, 10 Apr 2018 12:23:41 +0200 Subject: [PATCH] Add lint groups to doc export --- util/export.py | 1 + 1 file changed, 1 insertion(+) diff --git a/util/export.py b/util/export.py index 0607c864259..5419624d48e 100755 --- a/util/export.py +++ b/util/export.py @@ -18,6 +18,7 @@ This lint has the following configuration variables: def parse_lint_def(lint): lint_dict = {} lint_dict['id'] = lint.name + lint_dict['group'] = lint.group lint_dict['level'] = lint.level lint_dict['docs'] = {}