# HG changeset patch
# User wenzelm
# Date 1379503904 -7200
# Node ID 5ec27e55ddc2c5c644c5fd525f000556187924b0
# Parent  84522727f9d398121c69521c47f2dfff8e0c5c15
updated to polyml-5.5.1;

diff -r 84522727f9d3 -r 5ec27e55ddc2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Sep 18 13:18:51 2013 +0200
+++ b/src/Pure/ROOT.ML	Wed Sep 18 13:31:44 2013 +0200
@@ -79,7 +79,7 @@
 then use "ML/exn_trace_polyml-5.5.1.ML"
 else ();
 
-if ML_System.name = "polyml-5.5.0"
+if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";