author | wenzelm |
Mon, 23 Aug 2010 12:06:47 +0200 | |
changeset 38634 | bff9c05fe229 |
parent 38633 | 39412530436f |
child 38635 | f76ad0771f67 |
src/Pure/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/ROOT.ML Mon Aug 23 11:18:38 2010 +0200 +++ b/src/Pure/ROOT.ML Mon Aug 23 12:06:47 2010 +0200 @@ -179,7 +179,8 @@ use "ML/ml_syntax.ML"; use "ML/ml_env.ML"; use "Isar/runtime.ML"; -if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system +if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse + String.isPrefix "smlnj" ml_system then use "ML/ml_compiler.ML" else use "ML/ml_compiler_polyml-5.3.ML"; use "ML/ml_context.ML";