author | Fabian Huch <huch@in.tum.de> |
Tue, 09 Jan 2024 17:35:56 +0100 | |
changeset 79443 | 0d7c7fe65638 |
parent 78827 | 06f0e720b913 |
permissions | -rw-r--r-- |
78827
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
1 |
/* Title: Pure/Admin/component_javamail.scala |
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
2 |
Author: Fabian Huch, TU Muenchen |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
3 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
4 |
Build Isabelle java mail component (previously javax-mail, now jakarta + eclipse angus) |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
5 |
from official downloads. See also: |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
6 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
7 |
- https://jakarta.ee/specifications/mail |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
8 |
- https://mvnrepository.com/artifact/jakarta.mail/jakarta.mail-api |
78827
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
9 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
10 |
- https://jakarta.ee/specifications/activation |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
11 |
- https://mvnrepository.com/artifact/jakarta.activation/jakarta.activation-api |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
12 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
13 |
- https://eclipse-ee4j.github.io/angus-mail/ |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
14 |
- https://mvnrepository.com/artifact/org.eclipse.angus/angus-mail |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
15 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
16 |
- https://eclipse-ee4j.github.io/angus-activation/ |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
17 |
- https://mvnrepository.com/artifact/org.eclipse.angus/angus-activation |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
18 |
*/ |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
19 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
20 |
package isabelle |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
21 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
22 |
|
78827
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
23 |
object Component_Javamail { |
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
24 |
/* jars */ |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
25 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
26 |
sealed case class Jar(group_id: String, artifact_id: String, version: String) { |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
27 |
override def toString: String = group_id + ":" + artifact_id |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
28 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
29 |
def file_name: String = artifact_id + "-" + version + ".jar" |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
30 |
def maven_dir: String = group_id.replace('.', '/') + "/" + artifact_id + "/" + version |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
31 |
def url(repo_url: String): String = repo_url + "/" + maven_dir + "/" + file_name |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
32 |
} |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
33 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
34 |
val jars = |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
35 |
List( |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
36 |
Jar("jakarta.mail", "jakarta.mail-api", "2.1.2"), |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
37 |
Jar("jakarta.activation", "jakarta.activation-api", "2.1.2"), |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
38 |
Jar("org.eclipse.angus", "angus-mail", "2.0.2"), |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
39 |
Jar("org.eclipse.angus", "angus-activation", "2.0.1")) |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
40 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
41 |
|
78827
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
42 |
/* build javamail */ |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
43 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
44 |
val default_download_repo = "https://repo1.maven.org/maven2" |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
45 |
|
78827
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
46 |
def build_javamail( |
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
47 |
download_repo: String = default_download_repo, |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
48 |
progress: Progress = new Progress, |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
49 |
target_dir: Path = Path.current |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
50 |
): Unit = { |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
51 |
/* component */ |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
52 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
53 |
val component_name = "javamail-" + Date.Format.alt_date(Date.now()) |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
54 |
val component_dir = |
78827
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
55 |
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress) |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
56 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
57 |
File.write(component_dir.LICENSE, "See the file META-INF/LICENSE.txt in each jar file.") |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
58 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
59 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
60 |
/* README */ |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
61 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
62 |
File.write(component_dir.README, |
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
63 |
"This is " + component_name + " from\n" + download_repo + """ |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
64 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
65 |
See also: |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
66 |
- https://jakarta.ee/specifications/mail |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
67 |
- https://mvnrepository.com/artifact/jakarta.mail/jakarta.mail-api |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
68 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
69 |
- https://jakarta.ee/specifications/activation |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
70 |
- https://mvnrepository.com/artifact/jakarta.activation/jakarta.activation-api |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
71 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
72 |
- https://eclipse-ee4j.github.io/angus-mail/ |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
73 |
- https://mvnrepository.com/artifact/org.eclipse.angus/angus-mail |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
74 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
75 |
- https://eclipse-ee4j.github.io/angus-activation/ |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
76 |
- https://mvnrepository.com/artifact/org.eclipse.angus/angus-activation |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
77 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
78 |
|
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
79 |
Fabian |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
80 |
""" + Date.Format.date(Date.now()) + "\n") |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
81 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
82 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
83 |
/* settings */ |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
84 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
85 |
val settings = jars.map(jar => "\nclasspath \"$COMPONENT/lib/" + jar.file_name + "\"") |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
86 |
component_dir.write_settings(settings.mkString) |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
87 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
88 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
89 |
/* jars */ |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
90 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
91 |
Isabelle_System.make_directory(component_dir.lib) |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
92 |
for (jar <- jars) { |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
93 |
val path = component_dir.lib + Path.basic(jar.file_name) |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
94 |
Isabelle_System.download_file(jar.url(download_repo), path, progress = progress) |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
95 |
} |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
96 |
} |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
97 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
98 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
99 |
/* Isabelle tool wrapper */ |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
100 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
101 |
val isabelle_tool = |
78827
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
102 |
Isabelle_Tool("component_javamail", "build Isabelle javamail component from official download", |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
103 |
Scala_Project.here, |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
104 |
{ args => |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
105 |
var target_dir = Path.current |
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
106 |
var download_repo = default_download_repo |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
107 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
108 |
val getopts = Getopts(""" |
78827
06f0e720b913
added component for javax mail;
Fabian Huch <huch@in.tum.de>
parents:
77619
diff
changeset
|
109 |
Usage: isabelle component_javamail [OPTIONS] DOWNLOAD |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
110 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
111 |
Options are: |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
112 |
-D DIR target directory (default ".") |
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
113 |
-U URL download repository URL |
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
114 |
(default: """" + default_download_repo + """") |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
115 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
116 |
Build javamail component from the specified download repository (maven). |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
117 |
""", |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
118 |
"D:" -> (arg => target_dir = Path.explode(arg)), |
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
119 |
"U:" -> (arg => download_repo = arg)) |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
120 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
121 |
val more_args = getopts(args) |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
122 |
if (more_args.nonEmpty) getopts.usage() |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
123 |
|
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
124 |
val progress = new Console_Progress() |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
125 |
|
79443
0d7c7fe65638
update javamail component with current jakarta mail APIs and eclipse angus implementation;
Fabian Huch <huch@in.tum.de>
parents:
78827
diff
changeset
|
126 |
build_javamail(download_repo = download_repo, progress = progress, target_dir = target_dir) |
77619
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
127 |
}) |
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
wenzelm
parents:
diff
changeset
|
128 |
} |