summaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorIavor S. Diatchki <diatchki@galois.com>2012-10-04 16:39:28 -0700
committerIavor S. Diatchki <diatchki@galois.com>2012-10-04 16:39:28 -0700
commit5c2f21e06ebc2c3be936efadfe92872fecd82db9 (patch)
treecd9f7e158488fdf2380efb97aa6dfe6abc8a9bd0 /.gitignore
parentc97baa979878145c599c057d8bba01618c223178 (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