diff options
| author | Hugo Herbelin | 2016-10-08 22:51:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-09 08:13:18 +0200 |
| commit | b8ae2de5be242bbd1e34ec974627c81f99b16d23 (patch) | |
| tree | 6b6c2980e6aac60e53da6097dca7ae93db83d52e /lib/pp.mli | |
| parent | 8a8caba36ea6b0fd67e026ee3833d3b5b25af56d (diff) | |
Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
done by the Ppcmd_comment token) and so that lexing/parsing
side-effects are collected at the same place, i.e. in CLexer.
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 3bd560812e..f607e99dba 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -23,8 +23,7 @@ val ws : int -> std_ppcmds val mt : unit -> std_ppcmds val ismt : std_ppcmds -> bool -val comment : int -> std_ppcmds -val comments : ((int * int) * string) list ref +val comment : string list -> std_ppcmds (** {6 Manipulation commands} *) |