# HG changeset patch
# User wenzelm
# Date 1439905070 -7200
# Node ID 8fa408a560a5ac2746cf31d35dfa3662990d6e84
# Parent  24c53d220431f678c43b805e6ba6a69899941f26
SOMEthing went wrong in eb87fc42825c;

diff -r 24c53d220431 -r 8fa408a560a5 src/Pure/ML-Systems/windows_polyml.ML
--- a/src/Pure/ML-Systems/windows_polyml.ML	Tue Aug 18 15:08:22 2015 +0200
+++ b/src/Pure/ML-Systems/windows_polyml.ML	Tue Aug 18 15:37:50 2015 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML-Systems/ml_platform_path_polyml.ML
+(*  Title:      Pure/ML-Systems/windows_polyml.ML
     Author:     Makarius
 
 Poly/ML support for native Windows (MinGW).