From d361a57863fa46d49e39d63789382dd63414e3f3 Mon Sep 17 00:00:00 2001
From: Wenzel Jakob <wenzel.jakob@epfl.ch>
Date: Tue, 26 Apr 2016 00:12:22 +0200
Subject: [PATCH] minor mkdoc name sanitation fix

---
 tools/mkdoc.py | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/tools/mkdoc.py b/tools/mkdoc.py
index add11d4d..f5df6985 100644
--- a/tools/mkdoc.py
+++ b/tools/mkdoc.py
@@ -157,7 +157,10 @@ def extract(filename, node, prefix, output):
     if node.kind in PRINT_LIST:
         comment = d(node.raw_comment) if node.raw_comment is not None else ''
         comment = process_comment(comment)
-        name = sanitize_name(prefix + '_' + d(node.spelling))
+        sub_prefix = prefix
+        if len(sub_prefix) > 0:
+            sub_prefix += '_'
+        name = sanitize_name(sub_prefix + d(node.spelling))
         output.append('\nstatic const char *%s = %sR"doc(%s)doc";' % (name, '\n' if '\n' in comment else '', comment))
         num_extracted += 1
     return num_extracted