diff options
| author | Emilio Cobos Álvarez <emilio@crisal.io> | 2018-12-23 19:27:48 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-23 19:27:48 +0100 |
| commit | 2da6f06a711506a203078fb0be8f5b58fe15d73b (patch) | |
| tree | 7cb4464dd6a8cec538ad80eb679ccf6deb2a5910 /src/codegen/helpers.rs | |
| parent | d7dc5084402b6341db4869221969970beb374aa4 (diff) | |
| parent | 3923851bd1faea0f801bef1363ceebb07d23e1e1 (diff) | |
Merge pull request #1472 from emilio/record-matches-flag
Allow to turn off the matches recording introduced in #1469.
Diffstat (limited to 'src/codegen/helpers.rs')
0 files changed, 0 insertions, 0 deletions