diff options
| author | Maxime Dénès | 2018-02-28 09:59:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-28 09:59:44 +0100 |
| commit | 374e105be93beb2e9353bedf5cdd700a26308ebd (patch) | |
| tree | 5ffbb6fb23e3d418ed7d3eaec5360c7a69de9c1e /parsing/cLexer.ml4 | |
| parent | aec08b873425f6cdae4e1434651b4e9a97d0ced0 (diff) | |
| parent | d2293c3e1d51bdd2c25b203c655cc499e9bd5a91 (diff) | |
Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_state.
Diffstat (limited to 'parsing/cLexer.ml4')
| -rw-r--r-- | parsing/cLexer.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index f26398fa92..52a6fe16c6 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -404,8 +404,9 @@ let set_lexer_state (o,s,b,c,f) = between_commands := b; comments := c; current_file := f -let release_lexer_state () = +let get_lexer_state () = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file) +let release_lexer_state = get_lexer_state let drop_lexer_state () = set_lexer_state (init_lexer_state Loc.ToplevelInput) |