diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-04 18:59:33 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-04 18:59:33 +0000 |
| commit | 97f2f155ad238f48b35050088c3cf60cc326b1f3 (patch) | |
| tree | ec531843fb8a5ff2fd354ebaf87dfaa87db70c8b /src/main/main.h | |
| parent | a2cc0337aa53cfb686e26d68f98f2ae176ff1337 (diff) | |
Add documentation to Node and TNode (closes bug #201).
Also, only build doxygen documentation on stuff in src/,
not test/ or contrib/ or anywhere else. Hopefully this
turns our 3000+ page user manual into something a little
more useful!
Diffstat (limited to 'src/main/main.h')
| -rw-r--r-- | src/main/main.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/main/main.h b/src/main/main.h index 7e0bf6b65..b2e6e401b 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -47,6 +47,7 @@ extern CVC4::StatisticsRegistry* pStatistics; */ extern bool segvNoSpin; +/** The options currently in play */ extern Options options; /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ |