# HG changeset patch
# User wenzelm
# Date 1550155534 -3600
# Node ID 2156053c4ce903b9eee0019eb942e218feec585b
# Parent  a8debe27c36cadf22b46fb26b62125431cd19a5f
tuned according to Scala version;

diff -r a8debe27c36c -r 2156053c4ce9 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Thu Feb 14 15:44:02 2019 +0100
+++ b/src/Pure/PIDE/xml.ML	Thu Feb 14 15:45:34 2019 +0100
@@ -122,7 +122,7 @@
 
 (** string representation **)
 
-val header = "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n";
+val header = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n";
 
 
 (* escaped text *)