From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 17 Sep 2009 15:58:14 +0000
Subject: Delete trailing whitespaces in all *.{v,ml*} files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/profile.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib/profile.mli')

diff --git a/lib/profile.mli b/lib/profile.mli
index ab2af23985..3647756f71 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -49,7 +49,7 @@ let g = profile gkey g';;
 Before the program quits, you should call "print_profile ();;". It
 produces a result of the following kind:
 
-Function name              Own time Total time  Own alloc Tot. alloc     Calls 
+Function name              Own time Total time  Own alloc Tot. alloc     Calls
 f                            0.28      0.47        116        116      5      4
 h                            0.19      0.19          0          0      4      0
 g                            0.00      0.00          0          0      0      0
@@ -65,7 +65,7 @@ Est. overhead/total          0.00      0.47       2752       3260
   the number of calls to profiled functions inside the scope of the
   current function
 
-Remarks: 
+Remarks:
 
 - If a function has a polymorphic type, you need to supply it with at
   least one argument as in "let f a = profile1 fkey f a;;" (instead of
@@ -103,7 +103,7 @@ val profile6 :
     -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g
 val profile7 :
   profile_key ->
-  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) 
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h)
     -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
 
 
-- 
cgit v1.2.3