| author | wenzelm | 
| Thu, 30 Mar 2023 16:02:25 +0200 | |
| changeset 77763 | 2abc452d0ee9 | 
| parent 77759 | f513f754c026 | 
| child 77788 | c2ce9ac85859 | 
| permissions | -rw-r--r-- | 
| 
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 | 11  | 
/* resources */  | 
12  | 
||
13  | 
  def component_home: Path = Path.explode("$ISABELLE_RSYNC_HOME")
 | 
|
14  | 
||
15  | 
||
| 
77753
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
16  | 
/* build rsync */  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
17  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
18  | 
val default_version = "3.2.7"  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
19  | 
val default_download_url = "https://github.com/WayneD/rsync/archive/refs/tags"  | 
| 77755 | 20  | 
val default_build_options: List[String] =  | 
21  | 
List(  | 
|
| 77756 | 22  | 
"--disable-acl-support",  | 
| 77755 | 23  | 
"--disable-lz4",  | 
24  | 
"--disable-md2man",  | 
|
| 77756 | 25  | 
"--disable-openssl",  | 
26  | 
"--disable-xattr-support",  | 
|
27  | 
"--disable-xxhash",  | 
|
28  | 
"--disable-zstd")  | 
|
| 
77753
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
29  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
30  | 
def build_rsync(  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
31  | 
version: String = default_version,  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
32  | 
download_url: String = default_download_url,  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
33  | 
progress: Progress = new Progress,  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
34  | 
target_dir: Path = Path.current,  | 
| 77755 | 35  | 
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
 | 
36  | 
  ): Unit = {
 | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
37  | 
    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
 | 
38  | 
/* component */  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
39  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
40  | 
val component_name = "rsync-" + version  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
41  | 
val component_dir =  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
42  | 
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
 | 
43  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
44  | 
val platform_name =  | 
| 77763 | 45  | 
        proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
 | 
46  | 
          .getOrElse(error("No 64bit platform"))
 | 
|
| 
77753
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
47  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
48  | 
val platform_dir =  | 
| 77763 | 49  | 
        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
 | 
50  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
51  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
52  | 
/* download source */  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
53  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
54  | 
val archive_name = "v" + version + ".tar.gz"  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
55  | 
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
 | 
56  | 
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
 | 
57  | 
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
 | 
58  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
59  | 
Isabelle_System.extract(archive_path, tmp_dir)  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
60  | 
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
 | 
61  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
62  | 
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
 | 
63  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
64  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
65  | 
/* build */  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
66  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
67  | 
      progress.echo("Building rsync for " + platform_name + " ...")
 | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
68  | 
|
| 77756 | 69  | 
      val build_script = List("./configure " + Bash.strings(build_options.sorted), "make")
 | 
70  | 
      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
 | 
71  | 
progress_stdout = progress.echo(_, verbose = true),  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
72  | 
progress_stderr = progress.echo(_, verbose = true)).check  | 
| 
 
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  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
75  | 
/* install */  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
76  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
77  | 
      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
 | 
78  | 
      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
 | 
79  | 
|
| 
 
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  | 
/* settings */  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
82  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
83  | 
      component_dir.write_settings("""
 | 
| 
77757
 
49d38fa1478d
clarified directory names, following bash_process (see e59d7d6fe1bd);
 
wenzelm 
parents: 
77756 
diff
changeset
 | 
84  | 
ISABELLE_RSYNC_HOME="$COMPONENT"  | 
| 
 
49d38fa1478d
clarified directory names, following bash_process (see e59d7d6fe1bd);
 
wenzelm 
parents: 
77756 
diff
changeset
 | 
85  | 
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
 | 
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  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
89  | 
/* README */  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
90  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
91  | 
File.write(component_dir.README,  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
92  | 
"This is rsync " + version + " from " + download_url + """  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
93  | 
|
| 77756 | 94  | 
The distribution has been built like this:  | 
95  | 
||
96  | 
""" + ("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
 | 
97  | 
See also:  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
98  | 
* https://github.com/WayneD/rsync  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
99  | 
* https://rsync.samba.org  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
100  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
101  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
102  | 
Makarius  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
103  | 
""" + Date.Format.date(Date.now()) + "\n")  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
104  | 
}  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
105  | 
}  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
106  | 
|
| 
 
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  | 
/* Isabelle tool wrapper */  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
109  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
110  | 
val isabelle_tool =  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
111  | 
    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
 | 
112  | 
Scala_Project.here,  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
113  | 
      { args =>
 | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
114  | 
var target_dir = Path.current  | 
| 77755 | 115  | 
var build_options = default_build_options  | 
| 
77753
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
116  | 
var version = default_version  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
117  | 
var download_url = default_download_url  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
118  | 
var verbose = false  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
119  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
120  | 
        val getopts = Getopts("""
 | 
| 77755 | 121  | 
Usage: isabelle component_rsync [OPTIONS]  | 
| 
77753
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
122  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
123  | 
Options are:  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
124  | 
-D DIR target directory (default ".")  | 
| 77755 | 125  | 
-O OPT add build option  | 
126  | 
-R OPT remove build option  | 
|
| 
77753
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
127  | 
-U URL download URL  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
128  | 
(default: """" + default_download_url + """")  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
129  | 
-V VERSION version (default: """ + default_version + """)  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
130  | 
-v verbose  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
131  | 
|
| 77755 | 132  | 
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
 | 
133  | 
|
| 77755 | 134  | 
The default build options (for ./configure) are:  | 
135  | 
""" + 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
 | 
136  | 
"D:" -> (arg => target_dir = Path.explode(arg)),  | 
| 77755 | 137  | 
"O:" -> (arg => build_options = Library.insert(arg)(build_options)),  | 
138  | 
"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
 | 
139  | 
"U:" -> (arg => download_url = arg),  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
140  | 
"V:" -> (arg => version = arg),  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
141  | 
"v" -> (_ => verbose = true))  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
142  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
143  | 
val more_args = getopts(args)  | 
| 77755 | 144  | 
if (more_args.nonEmpty) getopts.usage()  | 
| 
77753
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
145  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
146  | 
val progress = new Console_Progress(verbose = verbose)  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
147  | 
|
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
148  | 
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
 | 
149  | 
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
 | 
150  | 
})  | 
| 
 
2b5b093a1c08
build rsync from sources, to avoid divergence of protocols on various platforms;
 
wenzelm 
parents:  
diff
changeset
 | 
151  | 
}  |