From 8a82af3511b4379af0d239dbd01c672c17a2c46a Mon Sep 17 00:00:00 2001 From: pukkandan Date: Fri, 27 May 2022 04:36:23 +0530 Subject: [cleanup] Misc fixes and cleanup Closes #3780, Closes #3853, Closes #3850 --- devscripts/make_readme.py | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'devscripts/make_readme.py') diff --git a/devscripts/make_readme.py b/devscripts/make_readme.py index 15c4a7c7d..42578cb0a 100755 --- a/devscripts/make_readme.py +++ b/devscripts/make_readme.py @@ -12,6 +12,8 @@ OPTIONS_START = 'General Options:' OPTIONS_END = 'CONFIGURATION' EPILOG_START = 'See full documentation' +DISABLE_PATCH = object() + def take_section(text, start=None, end=None, *, shift=0): return text[ @@ -21,7 +23,7 @@ def take_section(text, start=None, end=None, *, shift=0): def apply_patch(text, patch): - return re.sub(*patch, text) + return text if patch[0] is DISABLE_PATCH else re.sub(*patch, text) options = take_section(sys.stdin.read(), f'\n {OPTIONS_START}', f'\n{EPILOG_START}', shift=1) @@ -38,11 +40,15 @@ PATCHES = ( rf'({delim[:-1]})? (?P