diff options
| author | Chimrod <> | 2023-09-28 18:52:29 +0200 |
|---|---|---|
| committer | Chimrod <> | 2023-09-29 10:00:21 +0200 |
| commit | 71bdfc566bd50323695842a1c78007e1daac0e61 (patch) | |
| tree | ae729cf88703c4053da24836aa7c533369f9b687 /lib/dune | |
| parent | 93355b06a8270f02d345bdbe7b6a8c1bea9789bb (diff) | |
Added a way to discard the content until the end of the location — recover after an error
Diffstat (limited to 'lib/dune')
| -rw-r--r-- | lib/dune | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -1,8 +1,9 @@ (library (name qparser) (libraries - qsp_syntax + str menhirLib + qsp_syntax ) (preprocess (pps sedlex.ppx |