From da51e1bddf3f32d620ce94a9af768fa21d07a6f4 Mon Sep 17 00:00:00 2001
From: Holger Vogt <holger.vogt@uni-due.de>
Date: Wed, 28 Feb 2024 10:06:31 +0100
Subject: [PATCH] Don't use printf(".."), but fprintf(stdout, "..."), thus send
 an end-of-line also when redirected to file.

---
 src/frontend/device.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontend/device.c b/src/frontend/device.c
index b6af27493..d9b21dec5 100644
--- a/src/frontend/device.c
+++ b/src/frontend/device.c
@@ -854,7 +854,7 @@ listparam(wordlist *p, dgen *dg)
                 else
                     fprintf(cp_out, "%*.*s", LEFT_WIDTH, LEFT_WIDTH, " ");
                 k = dgen_for_n(dg, count, printvals_old, (plist + i), j);
-                printf("\n");
+                fprintf(cp_out,"\n");
                 j += 1;
             } while (k > 0);
         } else {