# HG changeset patch
# User wenzelm
# Date 1394487648 -3600
# Node ID d3c35a300433b531ede56bcfefd1c2a6de46bba1
# Parent  1403a22e5538248d2929f238c7ad3bf3318c0c42
proper Char comparison, despite weakly-typed Scala (cf. 5ff5208de089);

diff -r 1403a22e5538 -r d3c35a300433 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Mon Mar 10 22:39:37 2014 +0100
+++ b/src/Pure/General/completion.scala	Mon Mar 10 22:40:48 2014 +0100
@@ -217,7 +217,7 @@
     private def underscores: Parser[String] = "_*".r
 
     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
-    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == "."
+    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
 
     def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
     {