diff options
Diffstat (limited to 'ide/gtk_parsing.ml')
| -rw-r--r-- | ide/gtk_parsing.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index be5bb84e9..8da4d9dda 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -122,14 +122,14 @@ let find_comment_end (start:GText.iter) = let rec find_string_end (start:GText.iter) = - let backslash = int_of_char '\\' in - let rec escape c = - (c#char = backslash) && not (escape c#backward_char) + let dblquote = int_of_char '"' in + let rec escaped_dblquote c = + (c#char = dblquote) && not (escaped_dblquote c#backward_char) in match start#forward_search "\"" with | None -> raise Not_found | Some (stop,next_start) -> - if escape stop#backward_char + if escaped_dblquote stop#backward_char then find_string_end next_start else next_start |