summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2009-11-25 00:42:52 +0000
committerMorgan Deters <mdeters@gmail.com>2009-11-25 00:42:52 +0000
commit2a1ac62e56d43893c59c4c2d91bcaca0dd7ce417 (patch)
tree5d2e6b493d8d366ab75163effaf13191dbf0bd71 /src/main
parent06b391f721c8e9de4835e5a5bf2c60383ea7f8e9 (diff)
additional work on parser hookup, configuration + build
Diffstat (limited to 'src/main')
-rw-r--r--src/main/main.cpp3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 1fc616fe6..58d86a42d 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -71,9 +71,6 @@ int main(int argc, char *argv[]) {
cmd->invoke();
delete cmd;
}
-
- if(infile)
- infile.close();
} catch(CVC4::main::OptionException* e) {
if(opts.smtcomp_mode) {
printf("unknown");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback