diff options
Diffstat (limited to 'parsing/location.mli')
| -rw-r--r-- | parsing/location.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/parsing/location.mli b/parsing/location.mli index 354488226e..892c73c949 100644 --- a/parsing/location.mli +++ b/parsing/location.mli @@ -118,5 +118,4 @@ val report_error: formatter -> error -> unit val report_exception: formatter -> exn -> unit (* Reraise the exception if it is unknown. *) -val last_doc_token_loc: t ref - (* Remember the location of the last doc token. *) +val keep_doc_token: (t -> bool) ref |