# HG changeset patch
# User wenzelm
# Date 1492680816 -7200
# Node ID e307a781416ab86623dd779a64d4f2621eff8c05
# Parent  f47bc12b6e8a2ea1391fc04efdf41c5b731de5eb
tuned whitespace;

diff -r f47bc12b6e8a -r e307a781416a src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Apr 20 10:35:00 2017 +0200
+++ b/src/Pure/General/symbol.scala	Thu Apr 20 11:33:36 2017 +0200
@@ -216,7 +216,6 @@
         { case (List(a), Nil) => File(a) }))
     }
 
-
     def apply(text: CharSequence): Text_Chunk =
       new Text_Chunk(Text.Range(0, text.length), Index(text))
   }