diff options
| author | Iavor S. Diatchki <diatchki@galois.com> | 2012-10-04 16:39:28 -0700 |
|---|---|---|
| committer | Iavor S. Diatchki <diatchki@galois.com> | 2012-10-04 16:39:28 -0700 |
| commit | 5c2f21e06ebc2c3be936efadfe92872fecd82db9 (patch) | |
| tree | cd9f7e158488fdf2380efb97aa6dfe6abc8a9bd0 /.gitignore | |
| parent | c97baa979878145c599c057d8bba01618c223178 (diff) | |
Disable `tracing` by default.
To re-enable, turn on tracing in the parser file.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions