diff options
| author | Hugo Herbelin | 2018-12-12 23:41:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-12 23:41:11 +0100 |
| commit | 4ecbad30c77316294c8625ead722d469c1c7f79d (patch) | |
| tree | 5cb1d9e2d15149dfa4ee570bf8b78d03bf235723 /parsing/tok.mli | |
| parent | bb10141086110b8a736eb1e54292e5a48764f519 (diff) | |
| parent | c6b7a288eb9173b4b1c9df67230449fde42b9210 (diff) | |
Merge PR #9101: Fix 8922 again
Diffstat (limited to 'parsing/tok.mli')
| -rw-r--r-- | parsing/tok.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/tok.mli b/parsing/tok.mli index 55fcd33272..5750096a28 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -22,7 +22,8 @@ type t = | EOI val equal : t -> t -> bool -val extract_string : t -> string +(* pass true for diff_mode *) +val extract_string : bool -> t -> string val to_string : t -> string (* Needed to fit Camlp5 signature *) val print : Format.formatter -> t -> unit |