From: Brian Norris <banorris@uci.edu>
Date: Fri, 12 Oct 2012 17:21:41 +0000 (-0700)
Subject: mutex: define empty destructor
X-Git-Tag: pldi2013~48
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=51d0154de2ac3c660a58c3f377f4092c6fd1621b;ds=sidebyside

mutex: define empty destructor

I don't think we really need the destructor. It causes undefined
reference compilation errors though:

  ... undefined reference to `std::mutex::~mutex()'
---

diff --git a/include/mutex b/include/mutex
index 31fd7eb..482af59 100644
--- a/include/mutex
+++ b/include/mutex
@@ -18,7 +18,7 @@ namespace std {
 	class mutex {
 	public:
 		mutex();
-		~mutex();
+		~mutex() {}
 		void lock();
 		bool try_lock();
 		void unlock();