diff options
| author | Pierre-Marie Pédrot | 2019-03-31 23:07:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-31 23:07:48 +0200 |
| commit | 5dd3c18f4e50eef53ae4413b7b80951f17edad5f (patch) | |
| tree | 0a104d6afc109b7b89c8997d1afb3bc9f1e89dc3 /gramlib/plexing.ml | |
| parent | cb502e44aac8328ffd6c37429e050a01f72b2c53 (diff) | |
| parent | f832476404a29d7791c1a6d7970988d3b2e3ad9e (diff) | |
Merge PR #9733: [lexer] keyword protected quotation token for arbitrary text
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'gramlib/plexing.ml')
| -rw-r--r-- | gramlib/plexing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml index c294923a85..6da06f147f 100644 --- a/gramlib/plexing.ml +++ b/gramlib/plexing.ml @@ -2,7 +2,7 @@ (* plexing.ml,v *) (* Copyright (c) INRIA 2007-2017 *) -type pattern = string * string +type pattern = string * string option type location_function = int -> Loc.t type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function |