# HG changeset patch
# User Paul Boddie <paul@boddie.org.uk>
# Date 1526318219 -7200
# Node ID 527946fba4a1e6d15d1c0ebd54b9f30a39fdd572
# Parent  2c39f47138cf7587f759c1d77847445c17620587
Fixed the directory copy destination; added support for updating copied files.

diff -r 2c39f47138cf -r 527946fba4a1 tools/install.sh
--- a/tools/install.sh	Mon May 14 19:14:34 2018 +0200
+++ b/tools/install.sh	Mon May 14 19:16:59 2018 +0200
@@ -57,16 +57,19 @@
         TARGET="$OBJDIR/$OBJNAME"
 
         if [ "$CLEAN" ] ; then
-            if [ -d "$TARGET" ]; then
+            if [ -d "$TARGET" ] ; then
                 rm -r --one-file-system "$TARGET"
             else
                 rm "$TARGET"
             fi
         else
-            if [ -d "$ORIGIN" ]; then
-                cp -R "$ORIGIN" "$TARGET"
+            # With an existing target, attempt to update the installed objects.
+            # Otherwise, just install the objects.
+
+            if [ -d "$ORIGIN" ] ; then
+                cp -u -R "$ORIGIN" `dirname "$TARGET"`
             else
-                cp "$ORIGIN" "$TARGET"
+                cp -u "$ORIGIN" "$TARGET"
             fi
         fi
     done