From b6e45d75b3707626a78eecdb0ffd511008d9a006 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bob=20Dr=C3=B6ge?= <b.e.droge@rug.nl>
Date: Tue, 15 Jul 2025 13:58:18 +0200
Subject: [PATCH] use umask+cat instead of cp

---
 install_scripts.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/install_scripts.sh b/install_scripts.sh
index e1a5ac1a..e6220c2f 100755
--- a/install_scripts.sh
+++ b/install_scripts.sh
@@ -80,7 +80,8 @@ compare_and_copy() {
           else
             echo "File has changed in the PR"
           fi
-          cp "$source_file" "$destination_file"
+          # Use cat to retain existing permissions, set umask to world readable in case the target file does not yet exist.
+          (umask 022 && cat "$source_file" > "$destination_file")
           echo "File $source_file copied to $destination_file"
         else
           case $? in