From 7b10be9cb81be6ebf66f3d24ed4bf0e96ce34451 Mon Sep 17 00:00:00 2001
From: jancrichter <40425803+jancrichter@users.noreply.github.com>
Date: Thu, 18 Aug 2022 12:50:02 +0200
Subject: [PATCH] Append grep results to avoid overwriting header

Currently, if "keep_header" is true, the header is copied to the output file, but is then overwritten by the grep results.
---
 tools/filters/grep.xml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/filters/grep.xml b/tools/filters/grep.xml
index b3343f5bd93..ba65f014a75 100644
--- a/tools/filters/grep.xml
+++ b/tools/filters/grep.xml
@@ -17,7 +17,7 @@
     #else
       cat '$input'
     #end if
-    | grep -P -f '$pattern_file' $invert > '$out_file1'
+    | grep -P -f '$pattern_file' $invert >> '$out_file1'
   ]]></command>
   <configfiles>
     <configfile name="pattern_file">$pattern</configfile>