aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/lexer.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 1708fa5eb5..c241ca2842 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -95,7 +95,6 @@ let check_ident str =
bad_token str
| _ ->
bad_token str)
- (* iso 8859-1 accentuated letters *)
| [< _ = Stream.empty >] -> ()
| [< >] -> bad_token str
in