aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/tok.mli
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-10-05 08:16:42 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-10-05 08:16:42 +0200
commit2fb1f4f1bfdae2fe65c02048380fe8b6e619483e (patch)
tree848531635f96958a5b0762ea5d2170434e80138a /parsing/tok.mli
parent1969e10f25df0c913600099b7b98ea273a064017 (diff)
Revert "Move bullet detection from lexer to parser (bug #5102)."
Diffstat (limited to 'parsing/tok.mli')
-rw-r--r--parsing/tok.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/tok.mli b/parsing/tok.mli
index b1e79dc90..b9286c53e 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -16,6 +16,7 @@ type t =
| INT of string
| STRING of string
| LEFTQMARK
+ | BULLET of string
| EOI
val equal : t -> t -> bool