From e85efec7a57fc8acfa41d13815e9dec76acd4ebc Mon Sep 17 00:00:00 2001
From: "John J. Camilleri" <john@digitalgrammars.com>
Date: Fri, 20 Aug 2021 14:04:29 +0200
Subject: [PATCH] Do not copy when dest==dist in Setup.sh

---
 Setup.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Setup.sh b/Setup.sh
index 3d69081e..6a6a7c39 100755
--- a/Setup.sh
+++ b/Setup.sh
@@ -97,6 +97,7 @@ for module in $modules_alltenses; do
 done
 
 # Copy
+if [ $dest == $dist ]; then exit 0; fi
 echo "Copying to ${dest}"
 mkdir -p "${dest}"
 cp -R "${dist}"/* "${dest}"