projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 751539f) | patch
Add missing set of braces, fixes --trace.
authorMorgan Deters <mdeters@cs.nyu.edu>
Mon, 9 Jun 2014 15:05:35 +0000 (11:05 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Mon, 9 Jun 2014 15:11:19 +0000 (11:11 -0400)
commit5272664bcb8c85a81e9af8e61327797f3651c2c6
treeb6fcfb3f8d40b6a25590f2c3dd68328f366a590atree
parent751539f294fca0d039ccb748776c280e20cd9eabcommit | diff
Add missing set of braces, fixes --trace.

Also ensure // commented Debug() lines don't get included in Debug/Trace_tags.
src/options/Makefile.am diff | blob | history
src/options/base_options_handlers.h diff | blob | history