# HG changeset patch
# User wenzelm
# Date 1344109689 -7200
# Node ID bd4d132e32cf8d579d96eb860f31228c6740e65d
# Parent  3ef82491cdd6b326f3a1e8a8ce851162987d7ed5
tuned import;

diff -r 3ef82491cdd6 -r bd4d132e32cf src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sat Aug 04 21:45:41 2012 +0200
+++ b/src/Pure/PIDE/text.scala	Sat Aug 04 21:48:09 2012 +0200
@@ -10,7 +10,6 @@
 
 
 import scala.collection.mutable
-import scala.math.Ordering
 import scala.util.Sorting