# HG changeset patch
# User wenzelm
# Date 1750020930 -7200
# Node ID 85cf4336408028eb390b5df06f6cc6244e121ad9
# Parent  956ecf2c07a0aa7e993bdea26dbbcc0363c0530e
clarified signature;

diff -r 956ecf2c07a0 -r 85cf43364080 src/Pure/ML/ml_settings.scala
--- a/src/Pure/ML/ml_settings.scala	Sun Jun 15 22:46:45 2025 +0200
+++ b/src/Pure/ML/ml_settings.scala	Sun Jun 15 22:55:30 2025 +0200
@@ -29,7 +29,7 @@
     }
 }
 
-trait ML_Settings {
+abstract class ML_Settings {
   def polyml_home: Path
   def ml_system: String
   def ml_platform: String
@@ -48,4 +48,6 @@
 
   def polyml_exe: Path =
     ml_home + Path.basic("poly").exe_if(ml_platform_is_windows)
+
+  override def toString: String = ml_identifier
 }