From d6d4608eded24108e0a56101a1accd71abce7b72 Mon Sep 17 00:00:00 2001
From: Laurent Rineau <Laurent.Rineau__CGAL@normalesup.org>
Date: Mon, 26 Jan 2009 12:47:26 +0000
Subject: [PATCH] In CGAL::Profile_timer, use CGAL::Timer instead of
 CGAL::Real_timer, so that the CPU time is computed instead of the sum
 CPU+system times.

---
 Profiling_tools/include/CGAL/Profile_timer.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Profiling_tools/include/CGAL/Profile_timer.h b/Profiling_tools/include/CGAL/Profile_timer.h
index 2b103c627ec..9245b36047c 100644
--- a/Profiling_tools/include/CGAL/Profile_timer.h
+++ b/Profiling_tools/include/CGAL/Profile_timer.h
@@ -38,14 +38,14 @@
 #include <iostream>
 #include <iomanip>
 #include <string>
-#include <CGAL/Real_timer.h>
+#include <CGAL/Timer.h>
 
 CGAL_BEGIN_NAMESPACE
 
 struct Profile_timer
 {
     class Local {
-        Real_timer rt;
+        Timer rt;
         Profile_timer *p;
     public:
         Local(Profile_timer* p_) : p(p_) { rt.start(); }