Fix snapshot code
[model-checker.git] / output.h
index ca55b7a682352c9c67ad0d523a0f416d17991761..e390bb613510539958a1507eb2aaaddebd374ae3 100644 (file)
--- a/output.h
+++ b/output.h
@@ -5,8 +5,16 @@
 #ifndef __OUTPUT_H__
 #define __OUTPUT_H__
 
+#include "config.h"
+
+#ifdef CONFIG_DEBUG
+static inline void redirect_output() { }
+static inline void clear_program_output() { }
+static inline void print_program_output() { }
+#else
 void redirect_output();
 void clear_program_output();
 void print_program_output();
+#endif /* ! CONFIG_DEBUG */
 
 #endif /* __OUTPUT_H__ */