diff -r 096d83158d41 -r 81b47fc5c444 benchmark/bench_tools.h
--- a/benchmark/bench_tools.h	Fri Mar 02 17:56:22 2007 +0000
+++ b/benchmark/bench_tools.h	Fri Mar 02 18:04:28 2007 +0000
@@ -80,7 +80,7 @@
     }
 };
 
-inline void PrintTime(char *ID,lemon::Timer &T) 
+inline void PrintTime(const char *ID, lemon::Timer &T) 
 {
   lemon::TimeStamp S(T);
   std::cout << ID << ' ' << S.userTime() << ' '