From 7505813fa5f4d36274130c92be7e573b4aedb763 Mon Sep 17 00:00:00 2001
From: "John J. Camilleri" <john@digitalgrammars.com>
Date: Wed, 11 Nov 2020 21:58:45 +0100
Subject: [PATCH] Must make dest directory before copying to it

---
 .github/workflows/build.yml | 1 +
 Setup.sh                    | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 8231fab7..616911cb 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -19,6 +19,7 @@ jobs:
 
     - name: Build RGL
       run: |
+        mkdir -p ${DEST}
         bash Setup.sh --dest=${DEST} --gf=gf --verbose
 
     - name: Create archive
diff --git a/Setup.sh b/Setup.sh
index 6e8c5e1f..7141f68f 100755
--- a/Setup.sh
+++ b/Setup.sh
@@ -97,4 +97,4 @@ done
 
 # Copy
 echo "Copying to ${dest}"
-cp -R -p "${dist}"/* "${dest}"
+cp -R "${dist}"/* "${dest}"