# HG changeset patch
# User wenzelm
# Date 1677444920 -3600
# Node ID cd10b8edfdf50580834337868fafefacea2d6121
# Parent  cae3d891adfff323773837393b35f65bd3151343
clarified db content: avoid redundancy of historic ML_IDENTIFIER;

diff -r cae3d891adff -r cd10b8edfdf5 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Feb 26 21:17:10 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Feb 26 21:55:20 2023 +0100
@@ -255,10 +255,10 @@
 
     object Config {
       val instance = Generic.instance.make_primary_key
-      val ml_identifier = SQL.Column.string("ml_identifier")
+      val ml_platform = SQL.Column.string("ml_platform")
       val options = SQL.Column.string("options")
 
-      val table = make_table("", List(instance, ml_identifier, options))
+      val table = make_table("", List(instance, ml_platform, options))
     }
 
     object State {
@@ -424,7 +424,7 @@
     def write_config(db: SQL.Database, instance: String, hostname: String, options: Options): Unit =
       db.using_statement(Config.table.insert()) { stmt =>
         stmt.string(1) = instance
-        stmt.string(2) = Isabelle_System.getenv("ML_IDENTIFIER")
+        stmt.string(2) = Isabelle_System.getenv("ML_PLATFORM")
         stmt.string(3) = options.make_prefs(Options.init(prefs = ""))
         stmt.execute()
       }