equal
deleted
inserted
replaced
18 echo "Unknown destination directory for ${HOST}" |
18 echo "Unknown destination directory for ${HOST}" |
19 exit 2 |
19 exit 2 |
20 ;; |
20 ;; |
21 esac |
21 esac |
22 |
22 |
23 exec $(dirname $0)/mirror-isabelle-dist -d $DEST |
23 exec $(dirname $0)/rsync-isabelle -d $DEST |