1.1 --- a/tools/install.sh Mon May 14 19:14:34 2018 +0200
1.2 +++ b/tools/install.sh Mon May 14 19:16:59 2018 +0200
1.3 @@ -57,16 +57,19 @@
1.4 TARGET="$OBJDIR/$OBJNAME"
1.5
1.6 if [ "$CLEAN" ] ; then
1.7 - if [ -d "$TARGET" ]; then
1.8 + if [ -d "$TARGET" ] ; then
1.9 rm -r --one-file-system "$TARGET"
1.10 else
1.11 rm "$TARGET"
1.12 fi
1.13 else
1.14 - if [ -d "$ORIGIN" ]; then
1.15 - cp -R "$ORIGIN" "$TARGET"
1.16 + # With an existing target, attempt to update the installed objects.
1.17 + # Otherwise, just install the objects.
1.18 +
1.19 + if [ -d "$ORIGIN" ] ; then
1.20 + cp -u -R "$ORIGIN" `dirname "$TARGET"`
1.21 else
1.22 - cp "$ORIGIN" "$TARGET"
1.23 + cp -u "$ORIGIN" "$TARGET"
1.24 fi
1.25 fi
1.26 done