From 54617f34c441ea0baacf84f1d253e34a4cc402cc Mon Sep 17 00:00:00 2001
From: Janis Streib <janis.streib@kit.edu>
Date: Mon, 17 Feb 2025 12:44:53 +0100
Subject: [PATCH] FIX: don't exit on non-empty stderr

---
 dump.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dump.py b/dump.py
index 11ec300..a999c71 100644
--- a/dump.py
+++ b/dump.py
@@ -20,8 +20,8 @@ def exec_command_into_file(command: list[str], file: Optional[str], env: dict[st
         with open(file, 'w') as f:
             f.write(stdout.decode('utf-8'))
     if len(err.decode('utf-8')) > 0:
+        print(f'Warning: Captured non-empty STDERR while executing {command}')
         print(err.decode('utf-8'), file=sys.stderr)
-        sys.exit(1)
 
 def dump_data(main_version, obj, f_name, sort_key='name'):
 	d = None
-- 
GitLab