src/Pure/Admin/component_rsync.scala
author wenzelm
Sat, 08 Apr 2023 18:08:20 +0200
changeset 77788 c2ce9ac85859
parent 77763 2abc452d0ee9
child 80004 31ebb6be32b0
permissions -rw-r--r--
use remote copy of locally installed rsync component: for uniform version and options;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/component_rsync.scala
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     3
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     4
Build Isabelle rsync component from official source distribution.
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     5
*/
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     6
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     7
package isabelle
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     8
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
     9
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    10
object Component_Rsync {
77759
f513f754c026 more operations;
wenzelm
parents: 77757
diff changeset
    11
  /* resources */
f513f754c026 more operations;
wenzelm
parents: 77757
diff changeset
    12
77788
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77763
diff changeset
    13
  def home: Path = Path.explode("$ISABELLE_RSYNC_HOME")
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77763
diff changeset
    14
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77763
diff changeset
    15
  def local_program: Path = Path.explode("$ISABELLE_RSYNC")
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77763
diff changeset
    16
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77763
diff changeset
    17
  def remote_program(directory: Components.Directory): Path = {
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77763
diff changeset
    18
    val platform = "platform_" + directory.ssh.isabelle_platform.ISABELLE_PLATFORM64
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77763
diff changeset
    19
    directory.path + Path.basic(platform) + Path.basic("rsync")
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77763
diff changeset
    20
  }
77759
f513f754c026 more operations;
wenzelm
parents: 77757
diff changeset
    21
f513f754c026 more operations;
wenzelm
parents: 77757
diff changeset
    22
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    23
  /* build rsync */
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    24
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    25
  val default_version = "3.2.7"
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    26
  val default_download_url = "https://github.com/WayneD/rsync/archive/refs/tags"
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
    27
  val default_build_options: List[String] =
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
    28
    List(
77756
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
    29
      "--disable-acl-support",
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
    30
      "--disable-lz4",
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
    31
      "--disable-md2man",
77756
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
    32
      "--disable-openssl",
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
    33
      "--disable-xattr-support",
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
    34
      "--disable-xxhash",
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
    35
      "--disable-zstd")
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    36
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    37
  def build_rsync(
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    38
    version: String = default_version,
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    39
    download_url: String = default_download_url,
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    40
    progress: Progress = new Progress,
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    41
    target_dir: Path = Path.current,
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
    42
    build_options: List[String] = default_build_options
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    43
  ): Unit = {
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    44
    Isabelle_System.with_tmp_dir("build") { tmp_dir =>
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    45
      /* component */
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    46
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    47
      val component_name = "rsync-" + version
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    48
      val component_dir =
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    49
        Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    50
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    51
      val platform_name =
77763
2abc452d0ee9 tuned message;
wenzelm
parents: 77759
diff changeset
    52
        proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
2abc452d0ee9 tuned message;
wenzelm
parents: 77759
diff changeset
    53
          .getOrElse(error("No 64bit platform"))
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    54
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    55
      val platform_dir =
77763
2abc452d0ee9 tuned message;
wenzelm
parents: 77759
diff changeset
    56
        Isabelle_System.make_directory(component_dir.path + Path.basic("platform_" + platform_name))
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    57
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    58
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    59
      /* download source */
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    60
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    61
      val archive_name = "v" + version + ".tar.gz"
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    62
      val archive_path = tmp_dir + Path.explode(archive_name)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    63
      val archive_url = Url.append_path(download_url, archive_name)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    64
      Isabelle_System.download_file(archive_url, archive_path, progress = progress)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    65
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    66
      Isabelle_System.extract(archive_path, tmp_dir)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    67
      val source_dir = File.get_dir(tmp_dir, title = archive_url)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    68
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    69
      Isabelle_System.extract(archive_path, component_dir.src, strip = true)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    70
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    71
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    72
      /* build */
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    73
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    74
      progress.echo("Building rsync for " + platform_name + " ...")
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    75
77756
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
    76
      val build_script = List("./configure " + Bash.strings(build_options.sorted), "make")
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
    77
      Isabelle_System.bash(build_script.mkString(" && "), cwd = source_dir.file,
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    78
        progress_stdout = progress.echo(_, verbose = true),
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    79
        progress_stderr = progress.echo(_, verbose = true)).check
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    80
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    81
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    82
      /* install */
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    83
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    84
      Isabelle_System.copy_file(source_dir + Path.explode("COPYING"), component_dir.LICENSE)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    85
      Isabelle_System.copy_file(source_dir + Path.explode("rsync").platform_exe, platform_dir)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    86
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    87
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    88
      /* settings */
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    89
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    90
      component_dir.write_settings("""
77757
49d38fa1478d clarified directory names, following bash_process (see e59d7d6fe1bd);
wenzelm
parents: 77756
diff changeset
    91
ISABELLE_RSYNC_HOME="$COMPONENT"
49d38fa1478d clarified directory names, following bash_process (see e59d7d6fe1bd);
wenzelm
parents: 77756
diff changeset
    92
ISABELLE_RSYNC="$ISABELLE_RSYNC_HOME/platform_${ISABELLE_PLATFORM64}/rsync"
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    93
""")
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    94
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    95
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    96
      /* README */
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    97
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    98
      File.write(component_dir.README,
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
    99
        "This is rsync " + version + " from " + download_url + """
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   100
77756
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
   101
The distribution has been built like this:
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
   102
efd5c582d7ae tuned README;
wenzelm
parents: 77755
diff changeset
   103
""" + ("cd src" :: build_script).map(s => "  " + s + "\n").mkString + """
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   104
See also:
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   105
  * https://github.com/WayneD/rsync
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   106
  * https://rsync.samba.org
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   107
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   108
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   109
        Makarius
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   110
        """ + Date.Format.date(Date.now()) + "\n")
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   111
    }
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   112
}
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   113
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   114
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   115
  /* Isabelle tool wrapper */
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   116
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   117
  val isabelle_tool =
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   118
    Isabelle_Tool("component_rsync", "build rsync component from source distribution",
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   119
      Scala_Project.here,
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   120
      { args =>
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   121
        var target_dir = Path.current
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   122
        var build_options = default_build_options
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   123
        var version = default_version
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   124
        var download_url = default_download_url
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   125
        var verbose = false
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   126
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   127
        val getopts = Getopts("""
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   128
Usage: isabelle component_rsync [OPTIONS]
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   129
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   130
  Options are:
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   131
    -D DIR       target directory (default ".")
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   132
    -O OPT       add build option
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   133
    -R OPT       remove build option
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   134
    -U URL       download URL
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   135
                 (default: """" + default_download_url + """")
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   136
    -V VERSION   version (default: """ + default_version + """)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   137
    -v           verbose
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   138
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   139
  Build rsync component from the specified source distribution.
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   140
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   141
  The default build options (for ./configure) are:
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   142
""" + default_build_options.map(opt => "    " + opt + "\n").mkString,
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   143
          "D:" -> (arg => target_dir = Path.explode(arg)),
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   144
          "O:" -> (arg => build_options = Library.insert(arg)(build_options)),
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   145
          "R:" -> (arg => build_options = Library.remove(arg)(build_options)),
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   146
          "U:" -> (arg => download_url = arg),
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   147
          "V:" -> (arg => version = arg),
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   148
          "v" -> (_ => verbose = true))
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   149
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   150
        val more_args = getopts(args)
77755
12c8d72df48a clarified build options;
wenzelm
parents: 77754
diff changeset
   151
        if (more_args.nonEmpty) getopts.usage()
77753
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   152
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   153
        val progress = new Console_Progress(verbose = verbose)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   154
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   155
        build_rsync(version = version, download_url = download_url, progress = progress,
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   156
          target_dir = target_dir, build_options = build_options)
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   157
      })
2b5b093a1c08 build rsync from sources, to avoid divergence of protocols on various platforms;
wenzelm
parents:
diff changeset
   158
}