src/Tools/jEdit/patches/jedit-4.5.1/caret
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 47471 d6a1b5aeb4b1
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
--- 4.5.1/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2012-03-25 18:51:47.000000000 +0200
+++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2012-04-14 18:37:11.000000000 +0200
@@ -4907,7 +4907,7 @@
 	/**
 	 * Returns true if the caret is visible, false otherwise.
 	 */
-	final boolean isCaretVisible()
+	public final boolean isCaretVisible()
 	{
 		return blink && hasFocus();
 	} //}}}