diff --git a/src/timing/timing.c b/src/timing/timing.c
index f6c31cbf..556c405c 100644
--- a/src/timing/timing.c
+++ b/src/timing/timing.c
@@ -26,6 +26,8 @@
 
 #include "timing.h"
 
+/* see timing.h for an explanation of _mangle() */
+
 /* 
  * Returns milliseconds no matter what. 
  */
diff --git a/src/timing/timing.h b/src/timing/timing.h
index 8fa181b1..8e00c77e 100644
--- a/src/timing/timing.h
+++ b/src/timing/timing.h
@@ -11,6 +11,12 @@ typedef __int64 int64_t;
 typedef unsigned __int64 uint64_t;
 #endif
 
+/* config.h should be included before we are to define _mangle */
+#ifdef _mangle
+# define timing_get_time _mangle(timing_get_time)
+# define timing_sleep _mangle(timing_sleep)
+#endif
+
 uint64_t timing_get_time(void);
 void timing_sleep(uint64_t sleeptime);