summaryrefslogtreecommitdiff
path: root/src/util/statistics_registry.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-01-25 15:16:43 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-01-25 17:39:21 -0500
commit195dffbb7468e814d3dc3226666688869c13ba3d (patch)
tree4c4915245a90615ea36cbcfbb4a8a6dcc910c384 /src/util/statistics_registry.h
parent73760b3c213733fc98d67f9ceeb74d06b01a3777 (diff)
Fix errors and reduce warnings on clang (merge from mdeters/clang)
Diffstat (limited to 'src/util/statistics_registry.h')
-rw-r--r--src/util/statistics_registry.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 0a5450b8a..9aca3cb5a 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -42,6 +42,8 @@ namespace CVC4 {
class ExprManager;
class SmtEngine;
+inline std::ostream& operator<<(std::ostream& os, const timespec& t);
+
/**
* The base class for all statistics.
*
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback