src/Tools/jEdit/patches/jedit-4.5.1/caret
changeset 48789 7476665f3e0f
parent 48788 cea7f88c8084
parent 48787 ab3e7f40f341
child 48790 6e739225dd8a
child 48796 0f94b8b69e79
--- a/src/Tools/jEdit/patches/jedit-4.5.1/caret	Mon Aug 13 20:01:30 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-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();
- 	} //}}}