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 }