aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--[-rwxr-xr-x]ide/coq2.icobin4710 -> 4710 bytes
-rw-r--r--ide/wg_ScriptView.ml4
2 files changed, 1 insertions, 3 deletions
diff --git a/ide/coq2.ico b/ide/coq2.ico
index bc1732fd99..bc1732fd99 100755..100644
--- a/ide/coq2.ico
+++ b/ide/coq2.ico
Binary files differ
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 279815d671..181418d3d8 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -408,10 +408,8 @@ object (self)
| _ -> ()
method apply_unicode_binding () =
- (* Auxiliary method to reach the beginning of line or the
- nearest space before the iterator. *)
let rec get_line_start iter =
- if iter#starts_line || Glib.Unichar.isspace iter#char then iter
+ if iter#starts_line then iter
else get_line_start iter#backward_char
in
(* Main action *)