# HG changeset patch
# User wenzelm
# Date 1441741761 -7200
# Node ID dcbec1b22b07533751bf404eff2d874c380faaef
# Parent  4010e1559a2428af19b5ed50377e54e273e4752a
proper Windows path, notably for ML basis;

diff -r 4010e1559a24 -r dcbec1b22b07 src/Pure/ML/exn_properties_polyml.ML
--- a/src/Pure/ML/exn_properties_polyml.ML	Tue Sep 08 21:10:23 2015 +0200
+++ b/src/Pure/ML/exn_properties_polyml.ML	Tue Sep 08 21:49:21 2015 +0200
@@ -21,7 +21,7 @@
     [] => []
   | [XML.Text file] =>
       if file = "Standard Basis" then []
-      else [(Markup.fileN, file)]
+      else [(Markup.fileN, ml_standard_path file)]
   | body => XML.Decode.properties body);
 
 fun position_of loc =