aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-15 20:25:36 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-15 20:25:36 +0000
commit80c3103a85deb61ed37963bb114dad5901ca2c39 (patch)
tree4cbe46a792bf616201b63d87a9c7c8108a0353c3 /parsing
parentab1f9b9915059506e3982d7bee0cd4814aa70b08 (diff)
Bug (code prévu pour iso-latin et non utf-8)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7869 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/lexer.ml45
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index caae659ec..be52fa5f1 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -327,8 +327,9 @@ let parse_226_tail tk = parser
t = special (progress_special c3 (progress_special c2
(progress_special '\226' tk))) >] ->
TokSymbol t
- | [< len = ident_tail (store 0 '\226') >] ->
- TokIdent (get_buff len)
+ | [< '_; '_ >] ->
+ (* Unsupported utf-8 code *)
+ TokSymbol None
(* Parse what follows a dot *)