From e0d431cbc954c24f47dbeb80ddebe464f4e9899a Mon Sep 17 00:00:00 2001 From: Matthias Ringwald Date: Sun, 24 Dec 2017 00:35:42 +0100 Subject: [PATCH] docs: fix outline for ports section --- doc/manual/ports2markdown.py | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/doc/manual/ports2markdown.py b/doc/manual/ports2markdown.py index d00c1db18..5044c9477 100755 --- a/doc/manual/ports2markdown.py +++ b/doc/manual/ports2markdown.py @@ -54,14 +54,11 @@ def process_readmes(intro_file, port_folder, ports_file, ports_folder): for readme_dir, readme_file in sorted(matches.items()): with open(readme_file, 'rb') as fin: for line in fin: - #increase level of indetation + #increase level of indentation parts = re.match('#(.*)\n',line) title_parts = re.match('(#\s+)(.*)\n',line) - if parts: - if title_parts: - ports.write("## " + title_parts.group(2) + " {" + "#sec:" + readme_dir + "Port}\n" ) - else: - ports.write("## " + line) + if parts and title_parts: + ports.write("# " + title_parts.group(2) + " {" + "#sec:" + readme_dir + "Port}\n" ) else: ports.write(line)