From 4ede28040ccac8fc9bab86ef8d571838020f2a14 Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@iut-bm.univ-fcomte.fr>
Date: Tue, 27 Nov 2012 13:45:58 +0100
Subject: [PATCH 1/1] gras_os_time() has vanished.

---
 src/include/xbt/xbt_os_time.h | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/include/xbt/xbt_os_time.h b/src/include/xbt/xbt_os_time.h
index 3498cecd35..a86bcdd96c 100644
--- a/src/include/xbt/xbt_os_time.h
+++ b/src/include/xbt/xbt_os_time.h
@@ -15,8 +15,7 @@
 /** @brief get time in seconds 
 
   * gives  the  number  of  seconds since the Epoch (00:00:00 UTC, January 1, 1970).
-  * Most users should use gras_os_time and should not use this function unless 
-    they really know what they are doing. */
+  */
 XBT_PUBLIC(double) xbt_os_time(void);
 XBT_PUBLIC(void) xbt_os_sleep(double sec);
 
-- 
2.20.1