remove \r from output

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 16, 2022 · fe00e95 · fe00e95
1 parent 9d6de2f
commit fe00e95
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/doc/parameterhelp.py b/doc/parameterhelp.py
@@ -5,8 +5,9 @@
 
 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)