From 72364c1745644dd452cf40ef0a662bbaa9fd400f Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 3 Nov 2013 23:33:15 +0000
Subject: empty token in terminal is a user error not an anomaly (bug 3118)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17047 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/lexer.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index b476f5303..d37331449 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -673,7 +673,7 @@ let strip s =
 
 let terminal s =
   let s = strip s in
-  let () = match s with "" -> failwith "empty token" | _ -> () in
+  let () = match s with "" -> Errors.error "empty token." | _ -> () in
   if is_ident_not_keyword s then IDENT s
   else if is_number s then INT s
   else KEYWORD s
-- 
cgit v1.2.3