Download a file to a destination machine. This procedure returns either an empty string (indicating failure) or the name of the file on the destination macine.
remote_download dest file args
destDestination machine name.
fileFilename.
argsIf the optional destination filename is specified, that filename will be used on the destination machine.