Admin/mirror-dist
changeset 8398 f1c80ed70f48
parent 8397 f2d371bde3c4
child 10531 a9e7786db49e
--- a/Admin/mirror-dist	Thu Mar 09 17:25:28 2000 +0100
+++ b/Admin/mirror-dist	Thu Mar 09 17:27:54 2000 +0100
@@ -20,4 +20,4 @@
     ;;
 esac
 
-exec $(dirname $0)/mirror-isabelle-dist -d $DEST
+exec $(dirname $0)/rsync-isabelle -d $DEST