src/Pure/ML/ml_settings.scala
changeset 82721 85cf43364080
parent 82720 956ecf2c07a0
child 82729 d8986d88295e
--- 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
 }