summaryrefslogtreecommitdiff
path: root/src/parser/tptp/Tptp.g
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-08-16 15:15:03 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-09-13 18:32:39 -0400
commit14776d0aeb833a7e728a27af6ef545f20b495f7f (patch)
treeeccc91e0be00cfb9af7d757aae3dd07479c256fb /src/parser/tptp/Tptp.g
parent09fc93244e10b4450592b4ede151873142d54b34 (diff)
Documentation fixes, some code typo fixes, file perms, other minor things.
Diffstat (limited to 'src/parser/tptp/Tptp.g')
-rw-r--r--src/parser/tptp/Tptp.g2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 2ae31e810..61e0999e9 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -189,7 +189,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
}
*/
PARSER_STATE->includeFile(name /* , inclArgs */ );
- // The command of the included file will be produced at the new parseCommand call
+ // The command of the included file will be produced at the next parseCommand() call
cmd = new EmptyCommand("include::" + name);
}
| EOF
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback