From fe00e95f7239072ef07df9561c8e76dcda408c07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Aug 2022 09:20:50 -0700 Subject: [PATCH] remove \r from output Signed-off-by: Nikolaj Bjorner --- doc/parameterhelp.py | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/doc/parameterhelp.py b/doc/parameterhelp.py index 5fdd160ff..3edf9793e 100644 --- a/doc/parameterhelp.py +++ b/doc/parameterhelp.py @@ -5,8 +5,9 @@ import re Z3_EXE = "z3.exe" -def help(): - print("Z3 Options Enabled") +def help(ous): + + ous.write("Z3 Options\n") out = subprocess.Popen([Z3_EXE, "-pm"],stdout=subprocess.PIPE).communicate()[0] modules = [] if out != None: @@ -22,6 +23,8 @@ def help(): if out == None: continue out = out.decode(sys.stdout.encoding) - print(out) + out = out.replace("\r","") + ous.write(out) -help() +with open("Parameters.md",'w') as ous: + help(ous)