# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1698310431 -7200
# Node ID 348a5606baf3cf4b13c5decff107e92cf8df14c5
# Parent  58315c8a5cc4a6076b22bddb32257c68aed47b84
use mail module in CI build;

diff -r 58315c8a5cc4 -r 348a5606baf3 etc/options
--- a/etc/options	Tue Oct 24 19:17:46 2023 +0200
+++ b/etc/options	Thu Oct 26 10:53:51 2023 +0200
@@ -442,4 +442,3 @@
 option ci_mail_sender : string = "" for connection
 option ci_mail_smtp_host : string = "" for connection
 option ci_mail_smtp_port : int = 587 for connection
-option ci_mail_ssl : bool = true for connection
diff -r 58315c8a5cc4 -r 348a5606baf3 src/Pure/Admin/ci_build.scala
--- a/src/Pure/Admin/ci_build.scala	Tue Oct 24 19:17:46 2023 +0200
+++ b/src/Pure/Admin/ci_build.scala	Thu Oct 26 10:53:51 2023 +0200
@@ -50,6 +50,18 @@
     selection: Sessions.Selection = Sessions.Selection.empty)
 
 
+  def mail_server(options: Options): Mail.Server = {
+    val sender =
+      proper_string(options.string("ci_mail_sender")).map(Mail.address) getOrElse
+        Mail.default_address
+
+    new Mail.Server(sender,
+      smtp_host = options.string("ci_mail_smtp_host"),
+      smtp_port = options.int("ci_mail_smtp_port"),
+      user = options.string("ci_mail_user"),
+      password = options.string("ci_mail_password"))
+  }
+
   /* ci build jobs */
 
   sealed case class Job(name: String, description: String, profile: Profile, config: Build_Config) {