# HG changeset patch
# User wenzelm
# Date 1678529664 -3600
# Node ID b4ef44ce08edc72e0780b67062306c34b2a593ee
# Parent  236e43c8bb5b9d912226d6f98af7935280eb3645
do not export connection details (password etc.);

diff -r 236e43c8bb5b -r b4ef44ce08ed src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Mar 11 11:13:53 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Mar 11 11:14:24 2023 +0100
@@ -923,7 +923,7 @@
   final def start_build(): Unit = synchronized_database {
     for (db <- _database) {
       Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
-        store.options.make_prefs(Options.init(prefs = "")))
+        store.options.make_prefs(Options.init(prefs = ""), filter = _.is_exported))
     }
   }