summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-09-16 20:53:19 +0000
committerMorgan Deters <mdeters@gmail.com>2011-09-16 20:53:19 +0000
commit91e745e02684416186f4ea4e33cf8e42194cd7c9 (patch)
tree3002e7a61819275d97fa4220242bf07aa3cfaac7
parent55820808b55999c27ee1a66df0e674318302d5a6 (diff)
fix serious issue with copyright-updating script
-rwxr-xr-xcontrib/update-copyright.pl6
-rw-r--r--src/theory/shared_terms_database.cpp9
2 files changed, 12 insertions, 3 deletions
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 282bffd5d..397f1426b 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -170,6 +170,12 @@ sub handleFile {
print $OUT " **\n";
while(my $line = <$IN>) {
last if $line =~ /^ \*\*\s*$/;
+ if($line =~ /\*\//) {
+ print $OUT " ** [[ Add lengthier description here ]]\n";
+ print $OUT " ** \\todo document this file\n";
+ print $OUT $line;
+ last;
+ }
}
} else {
my $line = $_;
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 9ec421677..1687f3480 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -1,15 +1,18 @@
/********************* */
-/*! \file shared_terms_manager.cpp
+/*! \file shared_terms_database.cpp
** \verbatim
** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
**/
#include "theory/shared_terms_database.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback