From a5d792de61da02b5fdf68c599e88dd2e7d9aa56e Mon Sep 17 00:00:00 2001
From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Thu, 9 Jul 2015 14:44:58 +0200
Subject: [PATCH] [mc] Fix the DSO debug ignore list

This is nasty. We must get rid of this.
---
 buildtools/jenkins/build.sh | 2 ++
 src/mc/mc_process.cpp       | 3 ++-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/buildtools/jenkins/build.sh b/buildtools/jenkins/build.sh
index e6be9fa378..7226a67a2f 100755
--- a/buildtools/jenkins/build.sh
+++ b/buildtools/jenkins/build.sh
@@ -4,6 +4,8 @@ set -e
 
 build_mode="$1"
 
+echo "Build mode $build_mode on $(uname -np)" >&2
+
 # usage: die status message...
 die () {
   local status=${1:-1}
diff --git a/src/mc/mc_process.cpp b/src/mc/mc_process.cpp
index d5234e018c..5fee155143 100644
--- a/src/mc/mc_process.cpp
+++ b/src/mc/mc_process.cpp
@@ -44,12 +44,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc,
 // ***** Helper stuff
 
 #define SO_RE "\\.so[\\.0-9]*$"
-#define VERSION_RE "-[\\.0-9]*$"
+#define VERSION_RE "-[\\.0-9-]*$"
 
 static const char *const FILTERED_LIBS[] = {
   "libstdc++",
   "libboost_context",
   "libc++",
+  "libcdt",
   "libm",
   "libgcc_s",
   "libpthread",
-- 
2.20.1